-
research-article
The next 700 relational program logics
We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an algebraic ...
-
research-article
Dijkstra monads for all
- Kenji Maillard,
- Danel Ahman,
- Robert Atkey,
- Guido Martínez,
- Cătălin Hriţcu,
- Exequiel Rivas,
- Éric Tanter
This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We prove that any monad morphism between a ...
-
research-article
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise
- Carmine Abate,
- Arthur Azevedo de Amorim,
- Roberto Blanco,
- Ana Nora Evans,
- Guglielmo Fachini,
- Catalin Hritcu,
- Théo Laurent,
- Benjamin C. Pierce,
- Marco Stronati,
- Andrew Tolmach
We propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become compromised after encountering undefined behavior---for example, by ...
-
research-article
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
- Niklas Grimm,
- Kenji Maillard,
- Cédric Fournet,
- Cătălin Hriţcu,
- Matteo Maffei,
- Jonathan Protzenko,
- Tahina Ramananandro,
- Aseem Rastogi,
- Nikhil Swamy,
- Santiago Zanella-Béguelin
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the ...
-
research-article
Recalling a witness: foundations and applications of monotonic state
We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the current state, provided (1) state evolves according to a given preorder, ...
-
research-article
Verified low-level programming embedded in F*
- Jonathan Protzenko,
- Jean-Karim Zinzindohoué,
- Aseem Rastogi,
- Tahina Ramananandro,
- Peng Wang,
- Santiago Zanella-Béguelin,
- Antoine Delignat-Lavaud,
- Cătălin Hriţcu,
- Karthikeyan Bhargavan,
- Cédric Fournet,
- Nikhil Swamy
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently- typed ...
-
research-article
Dijkstra monads for free
- Danel Ahman,
- Cătălin Hriţcu,
- Kenji Maillard,
- Guido Martínez,
- Gordon Plotkin,
- Jonathan Protzenko,
- Aseem Rastogi,
- Nikhil Swamy
Dijkstra monads enable a dependent type theory to be enhanced with support for specifying and verifying effectful code via weakest preconditions. Together with their closely related counterparts, Hoare monads, they provide the basis on which ...
-
research-article
Beginner's luck: a language for property-based generators
- Leonidas Lampropoulos,
- Diane Gallois-Wong,
- Cătălin Hriţcu,
- John Hughes,
- Benjamin C. Pierce,
- Li-yao Xia
Property-based random testing à la QuickCheck requires building efficient generators for well-distributed random data satisfying complex logical predicates, but writing these generators can be difficult and error prone. We propose a domain-specific ...
-
research-article
Dependent types and multi-monadic effects in F*
- Nikhil Swamy,
- Cătălin Hriţcu,
- Chantal Keller,
- Aseem Rastogi,
- Antoine Delignat-Lavaud,
- Simon Forest,
- Karthikeyan Bhargavan,
- Cédric Fournet,
- Pierre-Yves Strub,
- Markulf Kohlweiss,
- Jean-Karim Zinzindohoue,
- Santiago Zanella-Béguelin
We present a new, completely redesigned, version of F*, a language that works both as a proof assistant as well as a general-purpose, verification-oriented, effectful programming language. In support of these complementary roles, F* is a dependently ...
-
invited-talk
Micro-Policies: Formally Verified, Tag-Based Security Monitors
Many of today's vulnerabilities arise from the violation of known, but in-practice unenforceable, safety and security policies, including high-level programming models and critical invariants of low-level programs. This project is aimed at showing that ...
-
research-article
Architectural Support for Software-Defined Metadata Processing
- Udit Dhawan,
- Catalin Hritcu,
- Raphael Rubin,
- Nikos Vasilakis,
- Silviu Chiricescu,
- Jonathan M. Smith,
- Thomas F. Knight,
- Benjamin C. Pierce,
- Andre DeHon
Optimized hardware for propagating and checking software-programmable metadata tags can achieve low runtime overhead. We generalize prior work on hardware tagging by considering a generic architecture that supports software-defined policies over ...
-
research-article
The Joint EasyCrypt-F*-CryptoVerif School 2014
Formal security verification tools are slowly reaching maturity. The Joint EasyCrypt-F*-CryptoVerif School took place between 24 and 28 November 2014 in Paris and taught participants how to use three state-of-the-art security verification tools, as well ...
-
research-article
A verified information-flow architecture
- Arthur Azevedo de Amorim,
- Nathan Collins,
- André DeHon,
- Delphine Demange,
- Cătălin Hriţcu,
- David Pichardie,
- Benjamin C. Pierce,
- Randy Pollack,
- Andrew Tolmach
SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible ...
-
research-article
Testing noninterference, quickly
- Catalin Hritcu,
- John Hughes,
- Benjamin C. Pierce,
- Antal Spector-Zabusky,
- Dimitrios Vytiniotis,
- Arthur Azevedo de Amorim,
- Leonidas Lampropoulos
Information-flow control mechanisms are difficult to design and labor intensive to prove correct. To reduce the time wasted on proof attempts doomed to fail due to broken definitions, we advocate modern random testing techniques for finding ...
-
research-article
Semantic subtyping with an SMT solver
We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core ...
-
research-article
Type-checking zero-knowledge
This paper presents the first type system for statically analyzing security protocols that are based on zero-knowledge proofs. We show how certain properties offered by zero-knowledge proofs can be characterized in terms of authorization policies and ...
