{"id":508007,"date":"2018-09-07T08:55:54","date_gmt":"2018-09-07T15:55:54","guid":{"rendered":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/?post_type=msr-research-item&p=508007"},"modified":"2018-09-27T10:02:27","modified_gmt":"2018-09-27T17:02:27","slug":"extending-f-in-f-proof-automation-and-metaprogramming-for-typeclasses-concurrency-optimizations-and-more-and-layered-dsls-for-verified-stateful-programming","status":"publish","type":"msr-video","link":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/video\/extending-f-in-f-proof-automation-and-metaprogramming-for-typeclasses-concurrency-optimizations-and-more-and-layered-dsls-for-verified-stateful-programming\/","title":{"rendered":"Extending F* in F*: Proof automation and Metaprogramming for Typeclasses, Concurrency, Optimizations and More and Layered DSLs for Verified Stateful Programming"},"content":{"rendered":"

Abstract for Talk Title 1: Extending F* in F*: Proof automation and Metaprogramming for Typeclasses, Concurrency, Optimizations and More<\/strong><\/p>\n

In this talk we will provide an overview of the road we’ve been following for the past year with Meta-F*, the tactics and metaprogramming engine for F*. While F* itself is a highly-automated theorem prover and program verifier, there are unavoidable limitations to its automation. Meta-F* aims to put the programmer in near full control of F*’s behaviour, allowing to nudge, tweak, twist and compose its internal components in a safe fashion.<\/p>\n

We introduce the “meta” into F* via a custom effect, making Meta-F* a part of F*, and not something above it. We provide several “hooks” into Meta-F*, allowing to preprocess or solve proof obligations, generate terms and top-level definitions, implement custom strategies for solving implicit arguments (birthing F*’s typeclasses), and transforming programs before extracting (to OCaml, F#, or C). We ensure the safety of these transformations by designing Meta-F* to closely follow F*’s static semantics. Further, metaprograms can be compiled and linked into the compiler, obtaining fast-and-safe extension capabilities for F*, and blurring the line between the compiler’s source code and Meta-F* metaprograms.<\/p>\n

We will describe some interesting use cases for Meta-F*, including arithmetic expression canonicalization, automated provably-memory-safe parser and printer generation, and some ongoing work in reasoning about concurrent programs in F*.<\/p>\n

Abstract for Talk Title 2: Layered DSLs for Verified Stateful Programming<\/strong><\/p>\n

Cryptographic code is security- and performance-critical and hence it calls for high-assurance, efficient implementations. However, optimized low-level code is not a good target for formal verification. To mitigate this, a two-layered verification approach is often employed: the efficient low-level code is shown to adhere to a high-level implementation, which is more amenable to formal verification. Low* is a subset of C, shallowly embedded in F*, that was build to assist this process. It gives access to the full memory model of C while supporting F*-style formal verification, allowing efficient crypto programs to be verified against their purely functional specs.<\/p>\n

This work aims to further reduce the gap between high-level code written with verification in mind and low-level code optimized for efficiency. In particular, following ideas from bidirectional programing, we allow the user to express their algorithms as pure programs that operate on some high-level, purely functional state that provides a view of C\u2019s memory. High-level programs written in this style enjoy a straight-forward interpretation as low-level programs. To further optimize these low-level programs we provide a set of rewrite rules whose soundness has been verified in F* and can be applied using F*\u2019s tactic engine, in order to obtain an efficient and correct by construction Low* program.<\/p>\n","protected":false},"excerpt":{"rendered":"

Abstract for Talk Title 1: Extending F* in F*: Proof automation and Metaprogramming for Typeclasses, Concurrency, Optimizations and More In this talk we will provide an overview of the road we’ve been following for the past year with Meta-F*, the tactics and metaprogramming engine for F*. While F* itself is a highly-automated theorem prover and […]<\/p>\n","protected":false},"featured_media":508013,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_hide_image_in_river":0,"footnotes":""},"research-area":[13560],"msr-video-type":[206954],"msr-locale":[268875],"msr-post-option":[],"msr-session-type":[],"msr-impact-theme":[],"msr-pillar":[],"msr-episode":[],"msr-research-theme":[],"class_list":["post-508007","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-research-area-programming-languages-software-engineering","msr-video-type-microsoft-research-talks","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/2zQLfQ7eyPA","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/508007","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":1,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/508007\/revisions"}],"predecessor-version":[{"id":508022,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/508007\/revisions\/508022"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/media\/508013"}],"wp:attachment":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/media?parent=508007"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=508007"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=508007"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=508007"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=508007"},{"taxonomy":"msr-session-type","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-session-type?post=508007"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=508007"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=508007"},{"taxonomy":"msr-episode","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-episode?post=508007"},{"taxonomy":"msr-research-theme","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-research-theme?post=508007"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}