F* (pronounced F star) is a general-purpose proof-oriented
programming language, supporting both purely functional and
effectful programming. It combines the expressive power of dependent
types with proof automation based on SMT solving and tactic-based
interactive theorem proving.
F* programs compile, by default, to OCaml. Various fragments of F*
can also be extracted to F#, to C or Wasm by a tool
called KaRaMeL,
or to assembly using
the Vale
toolchain. F* is implemented in F* and bootstrapped using OCaml.
F* is open source on GitHub and is under
active development by Microsoft Research,
Inria, and by the community.
F* is distributed under the Apache 2.0 license.
Binaries for Windows, Linux, and Mac OS X are posted regularly on the releases page on GitHub.
You can also install F* from OPAM, Docker, Nix, or build it from sources, by following the instructions in INSTALL.md.
An online
book Proof-oriented
Programming In F* is being written and regular updates are
posted online. You probably want to read it while trying out
examples and exercises in your browser by clicking the image below.
Low*
We also have a
tutorial that covers Low*, a low-level subset of F*, which can be compiled to C by KaRaMeL.
Course Material
F* courses are often taught at various seasonal schools. Lectures and course materials for some of them are
also a useful resource.
Embedding Proof-oriented Programming Languages in F*)
Online lectures at the Oregon Programming Language Summer School (2021): Lecture notes, slides, code
Formal Verification with F* and Meta-F*
Lectures and tutorial at ECI 2019: Lecture notes, slides, code
Verifying Low-Level Code for Correctness and Security
Lectures at the Oregon Programming Language Summer School (2019): Lecture notes, slides, code
Program Verification with F*
Course at 2018 EUTypes Summer School,
8-12 August, 2018, Ohrid, Macedonia Course material
F* is used in several projects in both industrial and academic settings.
We list a few of them here. If you are using F* in your project, please
let us know by writing to the fstar-mailing-list.
Project Everest
Project Everest is an umbrella project that develops high-assurance
secure communication software in F*. A big part of the development of F* has been motivated by the scenarios
that Project Everest targets. Several offshoots from Project Everest continue as their own projects, including
some of those listed below.
HACL*, ValeCrypt, and EverCrypt
HACL* is a library of high-assurance cryptographic primitives, written in F* and extracted to C.
ValeCrypt provides formally proven implementations of cryptographic primitives in Vale,
a framework for verified assembly language programming embedded in F*.
EverCrypt combines them into a single cryptographic provider.
Code from these projects is now used in production in several projects,
including Mozilla Firefox,
the Linux kernel,
Python,
mbedTLS, the Tezos blockchain,
the ElectionGuard electronic voting SDK, and the Wireguard VPN.
EverParse
EverParse is a parser generator for binary formats that produces C code extracted from formally proven F*.
Parsers from EverParse are used in production in several projects, including in Windows Hyper-V,
where every network packet passing through the Azure cloud platform is parsed and validated first by code generated by EverParse. EverParse is also used in other
production settings, including ebpf-for-windows.
F* is an active topic of research, both in the programming languages and formal methods community,
as well as from an application perspective in the security and systems communities.
We list a few of them below, with full citations to these papers available in this bibliography.
If you would like your paper included in this list, please contact fstar-maintainers@googlegroups.com.
The Design of F* and its DSLs
Dependent
Types and Multi-monadic Effects in F* (POPL 2016) This
is the canonical reference describing the F* system. The
language has evolved in significant ways since 2016,
however, its core design and implementation is based on
this paper.
Verified
Low-level Programming Embedded in F* (ICFP 2017) which
describes the Low* fragment of F* which is a low-level
subset of F* that can be compiled to C by KaRaMeL.
A
Verified, Efficient Embedding of a Verifiable Assembly
Language (POPL 2019) which describes the Vale
language, a verified assembly language embedded in F*.
Meta-F*:
Proof Automation with SMT, Tactics, and Metaprograms
(ESOP 2019) which describes MetaF*, a metaprogramming
system within F* used to implement various aspects of F*,
ranging from its tactic engine to its support for
typeclasses.
Programming
and Proving with Indexed Effects (TR 2021) which
describes the design of F*’s support for user-defined
effects and provides a calculus that describes the logical
core of F*.
Steel:
Proof-oriented Programming in a Dependently Typed
Concurrent Separation Logic (ICFP 2021), which
describes the Steel language and its use of the SteelCore
concurrent separation logic for proofs of imperative
programs with various forms of concurrency.
Semantics and Effects
Verifying
Higher-order Programs with the Dijkstra Monad (PLDI
2013), which introduces the concept of the Dijkstra monad,
a core feature of F*’s system of effects.
Dijkstra
Monads for Free (POPL 2017), which shows how to
automatically derive Dijkstra monads for a class of
computational monads using a continuation-passing
transformation
A Monadic
Framework for Relational Verification: Applied to Information
Security, Program Equivalence, and Optimizations (CPP
2018), which builds on the Dijkstra Monads for Free work to
construct a framework for proving properties that relate
multiple programs or program executions.
Dijkstra Monads
for All (ICFP 2019), which generalizes the notion of a
Dijkstra monad and shows how to systematically relate
computational and specificational monads via monad morphisms.
Recalling a
Witness: Foundations and Applications of Monotonic
State (POPL 2018), which describes the design of a
program logic for reasoning about programs whose state
evolves monotonically, e.g., where the state is an
append-only log. This logic underpins both Low* and
Steel.
SteelCore:
An Extensible Concurrent Separation Logic for Effectful
Dependently Typed Programs (ICFP 2020), which describes
the SteelCore concurrent separation logic, the basis of the
Steel DSL.
Applications in Security and Cryptography
Many papers applying F* in security and cryptography can be
found in
the Project
Everest bibliography. We mention a few prominent ones here
as well as other applications not related to Project Everest.
WYS*: A DSL for
Verified Secure Multi-party Computations (POST 2017),
which describes the WYS* language, a domain-specific language
for writing verified mixed-mode secure multi-party
computations.
Implementing
and Proving the TLS 1.3 Record Layer(S&P 2017), which
describes a verified implementaion of the TLS-1.3 record layer
in Low*.
HACL*: A
Verified Modern Cryptographic Library (CCS 2017), which
describes HACL*, a verified cryptographic library
implemented in Low*.
Formally
Verified Cryptographic Web Applications in WebAssembly
(S&P 2019), which develops LibSignal*, an implementation
of the Signal protocol in F* using HACL*, compiled to Wasm
by KaRaMeL.
EverCrypt:
A Fast, Verified, Cross-Platform Cryptographic
Provider (S&P 2020), a crypto provider combining C and
assembly code from HACL* and Vale, as well as some
applications built on top of it, including a verified
high-performance Merkle tree that was used in an initial
version of Microsoft Azure CCF.
HACL×N:
Verified Generic SIMD Crypto (for all your favorite
platforms) (CCS 2020), which metaprograms vectorized
versions of cryptographic primitives, enabling a
“write-once, get vectorized versions for free” style.
A
Security Model and Fully Verified Implementation for the IETF
QUIC Record Layer (S&P 2021), a verified implementation of
the QUIC record layer in Low* combined with the protocol logic
implemented in Dafny.
DICE*:
A Formally Verified Implementation of DICE Measured Boot
(USENIX Security 2021), which proves the correctness &
security of the DICE measured boot protocol for
micro-controllers, implemented in Low*, using EverCrypt and
EverParse.
DY*:
A Modular Symbolic Verification Framework for Executable
Cryptographic Protocol Code (Euro S&P 2021), a framework
for type-based symbolic security analysis of cryptographic
protocol implementations developed in F*.
A
Tutorial-Style Introduction to DY* (LNCS 2021), which is, yes,
a tutorial-style introduction to DY*.
An
In-Depth Symbolic Security Analysis of the ACME
Standard (CCS 2021), which proves the security of a
model of the ACME certificate issuance and management
protocol using DY*.
Noise*:
A Library of Verified High-Performance Secure Channel Protocol
Implementations (S&P 2022), which metaprograms provably
secure implementations for a family of secure channel
protocols.
TreeSync:
Authenticated Group Management for Messaging Layer
Security (USENIX Security 2023), a reference
implementation of MLS in F*, proven secure using the DY*
framework.
Modularity,
Code Specialization, and Zero-Cost Abstractions for Program
Verification (ICFP 2023), which describes
proof-engineering techniques used in HACL* for generic
implementations of cryptographic constructions that can be
specialized repeatedly to many concrete implementations in
C. The techniques used here led to the adoption of verified
cryptographic code into the libraries of the Python
programming language.
Verifying
Indistinguishability of Privacy-Preserving Protocols
(OOPSLA 2023), which provides a library called Waldo in F*
that enables proofs of indistinguishability over traces of
communication in networking protocols.
Comparse:
Provably Secure Formats for Cryptographic Protocols (CCS
2023), which provides a parsing library for data formats that
are appropriate for use with symbolic protocol
analyzers. Comparse provides bit-level precise accounting of
formats allowing the DY* protocol analysis framework to reason
about concrete messages and identify protocol flaws that it
previously would have missed.
Applications in Systems
Provably-Safe
Multilingual Software Sandboxing using WebAssembly (USENIX
2022), which describes a verified implementation of a sandbox
for WebAssembly modules in Low* and Rust.
FastVer:
Making Data Integrity a Commodity (SIGMOD 2021), which
formalizes a protocol for data integrity monitoring in F*.
FastVer2:
A Provably Correct Monitor for Concurrent, Key-Value
Stores (CPP 2022), which proves the correctness of a
low-level, concurrent implementation of the FastVer protocol
in Steel.
Applications in Parsing
EverParse:
Verified Secure Zero-Copy Parsers for Authenticated
Message Formats (USENIX Security 2019), which
describes the EverParse parser generator for parsing
binary formats, producing C code.
Hardening
Attack Surfaces with Formally Proven Binary Format
Parsers (PLDI 2022), which uses EverParse to harden
network packet parsers in Windows Network Virtualization
and Hyper-V.
ASN1*:
Provably Correct Non-Malleable Parsing for ASN.1 DER
(CPP 2022), which formalizes the ASN.1 DER format in F*
and proves the correctness of a parser for it in
EverParse.
Applications in Programming, Program Proof, and Program Analysis
Verified
Compilation of Space-Efficient Reversible Circuits (CAV
2018), which presents ReVerC, a compiler for reversible
circuits proven correct in F*.
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
(VSTTE 2020), which develops verified transformations
for assembly programs in the Vale framework.
Statically
verified refinements for multiparty protocols (OOPSLA
2020), which presents Session*, a session-typed programming
language for multiparty protocols, formalized in F*.
Verified
Functional Programming of an Abstract Interpreter (SAS
2021), which develops an abstract interpretation framework for
an imperative language with a very compact proof of soundness
developed in F*.
Catala:
a programming language for the law (ICFP 2021), where
core parts of the compiler are formalized and proven correct
in F*.
Verification of
a Merkle Patricia Tree Library Using F*, which ports a
Merkle tree library from OCaml to F*, finds and fixes a bug,
and eventually proves it correct.
Certified
mergeable replicated data types (PLDI 2022), which
presents PEEPUL, a framework in which to build replicated data
types for use in distributed programming, formalized in
F*.
Aeneas:
Rust verification by functional translation (ICFP
2022), which translates Rust into pure F* enabling
functional correctness proofs.
Q*:
Implementing Quantum Separation Logic in F* (PlanQC 2022),
which adapts the SteelCore separation logic for use with a
quantum programming language.
Pipit:
Reactive Systems in F* (Extended Abstract) (TyDe 2023),
which describes a embedded DSL for verifying reactive systems.
Securing
Verified IO Programs Against Unverified Code in F*
(POPL 2024), which presents SCIO*, a formally secure
compilation framework for statically verified programs
performing input-output (IO).
Miscellaneous
A
Theorem Proving Approach to Programming Language Semantics
(ICSE-SEET 2023), which reports on experiences teaching
operational, denotational, and axiomatic semantics to students
using F*.
Papers about an older version of F*
The first paper to introduce a system called F* was in
2011. Although the current version of F* was redesigned and
implemented in 2015, we include some of these older papers here
for completeness.
Secure
Distributed Programming with Value-dependent Types (ICFP
2011), a longer version of which also appeared
in JFP.
Self-certification:
bootstrapping certified typecheckers in F* with Coq (POPL
2012), which certifies the correctness of the F* typechecker by
programming it in F* itself and bootstrapping the process by
checking about 7GB of proof using Coq in about 24 machine-days
of compute time.
Fully
abstract compilation to JavaScript (POPL 2013), which
models a subset of JavaScript in F* and develops a secure
compiler from an ML-like language to JavaScript.
Gradual
typing embedded securely in JavaScript (POPL 2014),
which develops a source-to-source compiler for
JavaScript with defensive checks to ensure the soundness of
gradual typing in adversarial contexts, proven corrent in
F*.
Probabilistic
relational verification for cryptographic implementations
(POPL 2014), which develops RF*, a relational dialect of the
language useful for proving security properties like
noninterference and for game-based cryptographic proofs.
>>> Read full article>>>
Copyright for syndicated content belongs to the linked Source : Hacker News – https://www.fstar-lang.org/