Secure Distributed Programming with Value-dependent Types

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 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.
Document type :
Conference papers
16th ACM SIGPLAN International Conference on Functional Programming, Sep 2011, Tokyo, Japan. 2011


https://hal.inria.fr/inria-00596715
Contributor : Pierre-Yves Strub <>
Submitted on : Tuesday, November 8, 2011 - 11:24:41 AM
Last modification on : Tuesday, November 8, 2011 - 11:30:53 AM

File

fstar-icfp-2011.pdf
fileSource_public_author

Identifiers

  • HAL Id : inria-00596715, version 1

Collections

Citation

Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, et al.. Secure Distributed Programming with Value-dependent Types. 16th ACM SIGPLAN International Conference on Functional Programming, Sep 2011, Tokyo, Japan. 2011. <inria-00596715>

Export

Share

Metrics

Consultation de
la notice

199

Téléchargement du document

62