Types, compilers, and cryptography for secure distributed programming

Abstract : We are more and more dependent on our computing infrastructure, and yet its security is challenged every day. From a research viewpoint, a lot of progress in security has been made, using in particular formal methods and programming language techniques. This has lead us to a first few small, exemplary verified systems and protocols. In spite of these results, it is still hard to gain strong confidence that a program is correct and secure, and most of the software that we depend upon offers very few guarantees. In this thesis, we focus on language-based security by construction. We take as input the specification of a distributed computation involving multiple participants, together with its expected security properties. We then verify that this specification is sound, using static verification techniques such as type systems, and we then automatically generate a program for each participant. During this compilation process, we select adequate cryptographic and hardware mechanisms, such that the compiled programs correctly implement the computation with the required security properties.
Document type :
Theses
Complete list of metadatas

Cited literature [73 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00685356
Contributor : Jeremy Planul <>
Submitted on : Friday, April 13, 2012 - 8:19:26 PM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Long-term archiving on : Monday, November 26, 2012 - 2:35:58 PM

Identifiers

  • HAL Id : pastel-00685356, version 1

Collections

Citation

Jeremy Planul. Types, compilers, and cryptography for secure distributed programming. Programming Languages [cs.PL]. Ecole Polytechnique X, 2012. English. ⟨pastel-00685356⟩

Share

Metrics

Record views

496

Files downloads

365