Name
Abstract | ||
|---|---|---|
Relational program logics have been used for mechanizing formal proofs of various cryptographic constructions. With an eye towards scaling these successes towards end-to-end security proofs for implementations of distributed systems, we present RF*, a relational extension of F*, a general-purpose higher-order stateful programming language with a verification system based on refinement types. The distinguishing feature of F* is a relational Hoare logic for a higher-order, stateful, probabilistic language. Through careful language design, we adapt the F* typechecker to generate both classic and relational verification conditions, and to automatically discharge their proofs using an SMT solver. Thus, we are able to benefit from the existing features of F*, including its abstraction facilities for modular reasoning about program fragments. We evaluate RF* experimentally by programming a series of cryptographic constructions and protocols, and by verifying their security properties, ranging from information flow to unlinkability, integrity, and privacy. Moreover, we validate the design of RF* by formalizing in Coq a core probabilistic λ calculus and a relational refinement type system and proving the soundness of the latter against a denotational semantics of the probabilistic lambda λ calculus. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2535838.2535847 | POPL |
Keywords | Field | DocType |
cryptographic construction,probabilistic lambda,relational verification condition,probabilistic language,relational refinement type system,cryptographic implementation,careful language design,relational program logic,probabilistic relational verification,core probabilistic,relational hoare logic,relational extension | Codd's theorem,Relational calculus,Programming language,Computer science,Statistical relational learning,Hoare logic,Denotational semantics,Theoretical computer science,Soundness,Probabilistic logic,Satisfiability modulo theories | Conference |
Volume | Issue | ISSN |
49 | 1 | 0362-1340 |
Citations | PageRank | References |
24 | 1.57 | 37 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Barthe | 1 | 2337 | 152.36 |
| Cédric Fournet | 2 | 3698 | 213.79 |
| Benjamin Grégoire | 3 | 817 | 48.93 |
| Pierre-Yves Strub | 4 | 540 | 29.87 |
| Nikhil Swamy | 5 | 763 | 45.69 |
| Santiago Zanella Beguelin | 6 | 6073 | 475.81 |