back to listing index

F*: A Higher-Order Effectful Language Designed for Program Verification

[web search]
Original source (www.fstar-lang.org)
Tags: programming SML functional-programming ocaml f-sharp
Clipped on: 2017-10-30

Image (Asset 1/9) alt=

F* (pronounced F star) is an ML-like functional programming language aimed at program verification. Its type system includes polymorphism, dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml, F#, or C for execution.

The latest version of F* is written entirely in F*, and bootstraps in OCaml and F#. It is open source and under active development on GitHub. A detailed description of this new F* version is available in a POPL 2016 paper and a POPL 2017 one. You can learn more about F* by following the online tutorial. Materials from recent talks are available below. Read our blog to keep up to date with the latest news on F*.

The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 including the underlying cryptographic primitives. Moreover, while F* is extracted to OCaml by default, we are devising a subset of F* that can be compiled to C for efficiency.

Previous versions of F* could also be translated to JavaScript. We have used these previous versions in a number of projects, ranging from verifying implementations of cryptographic constructions and protocols, implementations of web browser extensions, formalizing the semantics of other languages (including JavaScript and a compiler from a subset of F* to JavaScript, and TS*, a secure subset of TypeScript), and even certifying the correctness of the core of F* type-checker itself.

Download


The sources of F* are hosted on GitHub. Binary packages are available for multiple platforms.

  • Image (Asset 2/9) alt=

    Click the image below to start the F* tutorial.

    Image (Asset 3/9) alt=

    F* is a state-of-the-art research project under active development; as such, it contains a number of known bugs.

    For documentation please refer to the tutorial and the GitHub wiki.

    If you encounter a problem with F*, we encourage you to report it to the GitHub issue tracker. Please understand that we may not have the necessary manpower to address new feature requests - as an open source project, we welcome your contributions to help improve F*.

    The fstar-club mailing list is dedicated to F* users. Here is where all F* announcements are made to the general public (e.g. for releases, new papers, etc) and where users can ask questions, ask for help, discuss, provide feedback, announce jobs requiring at least 10 years of F* experience, etc. List archives are public, but only members can post. Join here!

People


F* is a joint project between Microsoft Research, INRIA, and the community at large.

Current team


Past contributors


Papers


2017
[14] A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations (Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin), arXiv:1703.00055, 2017. [bibtex] [pdf]
[13] Recalling a Witness: Foundations and Applications of Monotonic State (Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy), arXiv:1707.02466, 2017. [bibtex] [pdf]
[12] Everest: Towards a Verified, Drop-in Replacement of HTTPS (Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué), In 2nd Summit on Advances in Programming Languages, 2017. [bibtex] [pdf]
[11] Dijkstra Monads for Free (Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), ACM, 2017. [bibtex] [pdf] [doi]
[10] Verified Low-Level Programming Embedded in F* (Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy), In 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP), 2017. (To appear) [bibtex] [pdf]
2016
[9] Dependent Types and Multi-Monadic Effects in F* (Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, Santiago Zanella-Béguelin), In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2016. [bibtex] [pdf]
2015
[8] Wys*: A Verified Language Extension for Secure Multi-party Computations (Aseem Rastogi, Nikhil Swamy, and Michael Hicks), 2015. [bibtex] [pdf]
2014
[7] Gradual typing embedded securely in JavaScript (Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman), In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Suresh Jagannathan, Peter Sewell, eds.), ACM, 2014. [bibtex] [pdf] [doi]
[6] Probabilistic relational verification for cryptographic implementations (Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin), In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Suresh Jagannathan, Peter Sewell, eds.), ACM, 2014. [bibtex] [pdf] [doi]
2013
[5] Fully Abstract Compilation to JavaScript (Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, Benjamin Livshits), In 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013. [bibtex] [pdf]
[4] Verifying Higher-order Programs with the Dijkstra Monad (Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, Benjamin Livshits), In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation, 2013. [bibtex] [pdf]
[3] Secure distributed programming with value-dependent types (Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang), In J. Funct. Program., volume 23, 2013. [bibtex] [pdf]
2012
[2] Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (Pierre-Yves Strub, Nikhil Swamy, Cedric Fournet, Juan Chen), In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012. [bibtex] [pdf]
2011
[1] Secure distributed programming with value-dependent types (Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang), In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (Manuel M. T. Chakravarty, Zhenjiang Hu, Olivier Danvy, eds.), ACM, 2011. [bibtex] [pdf] [doi]

Talks


Image (Asset 4/9) alt=