{"id":169556,"date":"2008-05-29T08:34:41","date_gmt":"2008-05-29T15:34:41","guid":{"rendered":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/project\/f7-refinement-types-for-f\/"},"modified":"2020-05-05T00:34:09","modified_gmt":"2020-05-05T07:34:09","slug":"f7-refinement-types-for-f","status":"publish","type":"msr-project","link":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/project\/f7-refinement-types-for-f\/","title":{"rendered":"F7: Refinement Types for F#"},"content":{"rendered":"

F7 is an enhanced typechecker for the F#<\/a> programming language, a dialect of ML. F7 pioneers the static checking of security properties expressed with refinement types. Although the original motivation was to check security properties, F7 is not security-specific and is applied in other areas, such as database modelling.<\/p>\n

The theoretical core of F7 is the typed lambda-calculus Refined Concurrent FPC, or RCF for short. FPC itself is Plotkin and Gunter’s lambda-calculus with function, sum, product, unit, and recursive types. Refinement types are types qualified by logical formulas, also known as subset types. For example, x:int {x>0}, is the type of positive integers. RCF consists of FPC plus refinement types, dependent function and pair types, and concurrency in the style of the pi-calculus.<\/p>\n

The F7 implementation checks ordinary F# source code against enhanced F7 interface files. During typechecking F7 generates proof obligations that are passed to the Z3 SMT solver. The F7 download includes binaries, Visual Studio support, a range of sample protocols and libraries, and the source code of F7 itself.<\/p>\n

Our work on checking F# implementations of cryptographic software with F7, builds on prior work on FS2PV, developed in the Samoa<\/a> project, which checks F# by compiling to the ProVerif (opens in new tab)<\/span><\/a> tool. F7 descends from the Cryptyc (opens in new tab)<\/span><\/a> typechecker, which used dependent types to analyze security protocols, but which checked abstract process calculus models rather than executable F# code. Together with other tools, F7 is a constituent of the Cryptographic Verification Kit (CVK) developed at MSR Cambridge<\/a> and the MSR-INRIA Joint Centre. The most substantial application of F7 is to the cryptographic verification of miTLS (opens in new tab)<\/span><\/a>, a reference implementation of TLS 1.2; miTLS consists of 5KLOC\u00a0in F# together 2.5KLOC of F7 interface annotations.\u00a0The use of refinement types in F7 was inspired by the Sage (opens in new tab)<\/span><\/a> programming language. Some related security-oriented programming languages include AURA (opens in new tab)<\/span><\/a> and Fine<\/a>, and Dsolve (opens in new tab)<\/span><\/a> is another recent system of refinement types for ML. The F5 (opens in new tab)<\/span><\/a> tool-chain is an independent implementation of RCF, enriched with union, intersection, and polymorphic types. F*<\/a> is a more recent language that unifies and extends (opens in new tab)<\/span><\/a> most features of Fine and F7.<\/p>\n

F7 started in January 2007 as a project at MSR Cambridge<\/a>, led by researchers K. Bhargavan, C. Fournet, and A.D. Gordon, and with the help of our external colleagues J. Bengtson and S. Maffeis. Since then we’ve had help from many collaborators, especially those at the MSR-INRIA Joint Center.<\/p>\n","protected":false},"excerpt":{"rendered":"

F7 is an enhanced typechecker for the F# programming language, a dialect of ML. F7 pioneers the static checking of security properties expressed with refinement types. Although the original motivation was to check security properties, F7 is not security-specific and is applied in other areas, such as database modelling. The theoretical core of F7 is […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560,13558],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-169556","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-research-area-security-privacy-cryptography","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2008-05-29","related-publications":[153274,158401,166486,166720,166721],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[],"msr_research_lab":[],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169556","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":2,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169556\/revisions"}],"predecessor-version":[{"id":656274,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169556\/revisions\/656274"}],"wp:attachment":[{"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/media?parent=169556"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=169556"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=169556"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=169556"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/newed.any0.dpdns.org\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=169556"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}