Secure Distributed Programming with Value-Dependent Types - Archive ouverte HAL Access content directly
Journal Articles Journal of Functional Programming Year : 2013

Secure Distributed Programming with Value-Dependent Types

(1) , (1) , (2) , (3) , (4) , (5)
1
2
3
4
5
Nikhil Swamy
  • Function : Author
  • PersonId : 901972
Juan Chen
  • Function : Author
  • PersonId : 901973
Pierre-Yves Strub
  • Function : Author
  • PersonId : 857170
Karthikeyan Bhargavan
Jean Yang
  • Function : Author
  • PersonId : 901975

Abstract

Distributed 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 ver- ification 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. Our language 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 mechanized in Coq) and logical consistency for F⋆. We have implemented a compiler that translates F⋆ to .NET bytecode, based on a prototype for Fine. F⋆ provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. The compiler produces verifiable binaries with 60% code size overhead for proofs and types, as much as a 45x improvement over the Fine compiler, while still enabling efficient bytecode verification. We have programmed and verified nearly 50,000 lines of F⋆ including new schemes for multi- party sessions; a zero-knowledge privacy-preserving payment protocol; a provenance-aware curated database; a suite of web-browser extensions verified for authorization properties; a cloud-hosted multi-tier web application with a verified reference monitor; the core F⋆ typechecker itself; and programs translated to F⋆ from other languages such as F7 and JavaScript.
Fichier principal
Vignette du fichier
secure-distributed-programming-with-value-dependent-types-jfp-1.pdf (493.7 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00939188 , version 1 (11-04-2016)

Identifiers

  • HAL Id : hal-00939188 , version 1

Cite

Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, et al.. Secure Distributed Programming with Value-Dependent Types. Journal of Functional Programming, 2013, 23 (4), pp.402-451. ⟨hal-00939188⟩
159 View
319 Download

Share

Gmail Facebook Twitter LinkedIn More