Secure Distributed Programming with Value-dependent Types

Related Projects * F*: A Verifying ML Compiler for Distributed ProgrammingInternational audienceDistributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications and proofs becomes challenging. We present F, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Unlike prior languages, F provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F and controls their interaction. F subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs partially mechanized in Coq) and logical consistency for F