Search

OAEP is a widely used public-key encryption scheme based on trapdoor permutations. Its security proof has been scrutinized and amended repeatedly. Fifteen years after the introduction of OAEP, we present a machine-checked proof of its security against adaptive chosen-ciphertext attacks under the assumption that the underlying permutation is partial-domain one-way. The proof can be independently verified by running a small and trustworthy proof checker and fixes minor glitches that have subsisted in published proofs. We provide an overview of the proof, highlight the differences with earlier works, and explain in some detail a crucial step in the reduction: the elimination of indirect queries made by the adversary to random oracles via the decryption oracle. We also provide–within the limits of a conference paper–a broader perspective on independently verifiable security proofs. [ABSTRACT FROM AUTHOR]

Termination of recursive functions is an important property in proof assistants based on dependent type theories; it implies consistency and decidability of type checking. Type-based termination is a mechanism for ensuring termination that uses types annotated with size information to check that recursive calls are performed on smaller arguments. Our long-term goal is to extend the Calculus of Inductive Constructions with a type-based termination mechanism and prove its logical consistency. In this paper, we present an extension of the Calculus of Constructions (including universes and impredicativity) with sized natural numbers, and prove strong normalization and logical consistency. Moreover, the proof can be easily adapted to include other inductive types. [ABSTRACT FROM AUTHOR]

CertiCrypt is a general framework to certify the security of cryptographic primitives in the Coq proof assistant. CertiCrypt adopts the code-based paradigm, in which the statement of security, and the hypotheses under which it is proved, are expressed using probabilistic programs. It provides a set of programming language tools (observational equivalence, relational Hoare logic, semantics-preserving program transformations) to assist in constructing proofs. Earlier publications of CertiCrypt provide an overview of its architecture and main components, and describe its application to signature and encryption schemes. This paper describes programming language techniques that arise specifically in cryptographic proofs. The techniques have been developed to complete a formal proof of IND-CCA security of the OAEP padding scheme. In this paper, we illustrate their usefulness for showing the PRP/PRF Switching Lemma, a fundamental cryptographic result that bounds the probability of an adversary to distinguish a family of pseudorandom functions from a family of pseudorandom permutations. [ABSTRACT FROM AUTHOR]

Coq has within its logic a programming language that can be used to replace many deduction steps into a single computation, this is the so-called reflection. In this paper, we present two extensions of the evaluation mechanism that preserve its correctness and make it possible to deal with cpu-intensive tasks such as proof checking of SAT traces. [ABSTRACT FROM AUTHOR]

In Type Theory, definition by dependently-typed case analysis can be expressed by means of a set of equations – the semantic approach – or by an explicit pattern-matching construction – the syntactic approach. We aim at putting together the best of both approaches by extending the pattern-matching construction found in the Coq proof assistant in order to obtain the expressivity and flexibility of equation-based case analysis while remaining in a syntax-based setting, thus making dependently-typed programming more tractable in the Coq system. We provide a new rule that permits the omission of impossible cases, handles the propagation of inversion constraints, and allows to derive Streicher΄s K axiom. We show that subject reduction holds, and sketch a proof of relative consistency. [ABSTRACT FROM AUTHOR]

Certificate translation is a method that transforms certificates of source programs into certificates of their compilation. It provides strong guarantees on low-level code, and is useful for eliminating trust in the compiler (for high assurance code) and in the code producer for mobile code security. The theory of certificate translation has been developed in earlier work, but no implementation exists. As a result, it has been difficult to evaluate its practicality, and in particular the impact of certificate translation on the size of certificates. In this paper, we report on the development of a certificate translator prototype. The tool takes as input a high-level program, defined in a small subset of the C programming language, and a logical specification à la ACSL, and computes a set of verification conditions for the Coq proof assistant. Once proof obligations are discharged, the tool compiles the source program into an intermediate RTL (i.e., three-address code) representation, and then performs a sequence of compiler optimizations. At each step, certificates are transformed automatically to produce a proof for the transformed programs. For optimizations that rely on arithmetic reasoning, such as constant propagation and common subexpression, the tool implements a new certificate translation strategy that minimizes certificate growth. [ABSTRACT FROM AUTHOR]

CertiCrypt [1] is a framework that assists the construction of machine-checked cryptographic proofs that can be automatically verified by third parties. To date, CertiCrypt has been used to prove formally the exact security of widely studied cryptographic systems, such as the OAEP padding scheme and the Full Domain Hash digital signature scheme. The purpose of this article is to provide a gentle introduction to CertiCrypt. For concreteness, we focus on a simple but illustrative example, namely the semantic security of the Hashed ElGamal encryption scheme in both, the standard and the random oracle model. [ABSTRACT FROM AUTHOR]

Type-based termination is a method to enforce termination of recursive definitions through a non-standard type system that introduces a notion of size for inhabitants of inductively defined types. The purpose of this tutorial is to provide a gentle introduction to a polymorphically typed λ-calculus with type-based termination, and to the size inference algorithm which is used to guarantee automatically termination of recursive definitions. [ABSTRACT FROM AUTHOR]

The goal of the MOBIUS project is to develop a Proof Carrying Code architecture to secure global computers that consist of Java-enabled mobile devices. In this overview, we present the consumer side of the MOBIUS Proof Carrying Code infrastructure, for which we have developed formally certified, executable checkers. We consider wholesale Proof Carrying Code scenarios, in which a trusted authority verifies the certificate before cryptographically signing the application. We also discuss retail Proof Carrying Code, where the verification is performed on the consumer device. [ABSTRACT FROM AUTHOR]

Type-based termination is a semantically intuitive method that ensures termination of recursive definitions by tracking the size of datatype elements, and by checking that recursive calls operate on smaller arguments. However, many systems using type-based termination rely on a semantical anomaly to guarantee strong normalization; namely, they impose that non-recursive elements of a datatype, e.g. the empty list, have size 1 instead of 0. This semantical anomaly also prevents functions such as quicksort to be given a precise typing. The main contribution of this paper is a type system that remedies this anomaly, and still ensures termination. In addition, our type system features prenex stage polymorphism, a weakening of existential quantification over stages, and is precise enough to type quicksort as a non-size increasing function. Moreover, our system accomodate stage addition with all positive inductive types. [ABSTRACT FROM AUTHOR]

In Proof-Carrying Code, the verification condition generator (VCgen) generates a set of formulas whose validity implies that the code satisfies the consumer policy. Applying a VCgen to a bytecode language with exceptions (such as Java bytecode) can result in a large number of proof obligations, due to the amount of branching instructions. We present a VCgen for Java bytecode that uses static analyses to reduce the number of proof obligations. As a result, the task of producing a proof is simpler, and the subsequent proof terms smaller. We formalize the VCgen as a deep embedding in Coq and prove soundness with respect to the Bicolano formalization of the Java bytecode semantics. [ABSTRACT FROM AUTHOR]

While program verification environments typically target source programs, there is an increasing need to provide strong guarantees for executable programs. We establish that it is possible to reuse the proof that a source Java program meets its specification to show that the corresponding JVM program, obtained by non-optimizing compilation, meets the same specification. More concretely, we show that verification condition generators for Java and JVM programs generate the same set of proof obligations, when applied to a program p and its compilation [[p]] respectively. Preservation of proof obligations extends the applicability of Proof Carrying Code, by allowing certificate generation to rely on existing verification technology. [ABSTRACT FROM AUTHOR]

We give an overview of an application of the B method to the formalisation and verification of the GlobalPlatform Card Specification. Although there exists a semi-formal specification and some effort has been put into providing formalisations of particular features of smart card platforms, this is, as far as we know, the very first attempt to provide a complete formalisation. We describe the process followed to synthesise a mathematical model of the platform in the B language, starting from requirements stated in natural language. The model consistency has been thoroughly verified using formal techniques supported by the B method. We also discuss how the smart card industry might benefit from exploiting this formal specification and outline directions for future work. [ABSTRACT FROM AUTHOR]

Abstract interpretation is a particularly well-suited methodology to build modular correctness proof of static analysers. Proof modularity becomes essential when correctness proof is machine checked for realistic languages To deal with complex concrete and abstract domains, the notion of parameterised concretization has been proposed to allow a structural decomposition of the abstract domain and its concretization. In this paper we develop proof principles for such concretizations, based on the theoretical notion of concretization functor, with the aim of obtaining modular correctness proofs. Our technique has been tested on a machine-checked correctness proof of a static analysis for a Java-like bytecode language. [ABSTRACT FROM AUTHOR]

Multi-Processor Systems-on-Chips (MPSoCs) gather multiple processors and hardware accelerators in a single chip to meet the performance and energy consumption requirements of mobile devices. To follow the rapid evolution of such applications, the MPSoC community need flexible and programmable platforms intended to be diverted to many use cases, and hence consider definitely the software as one of the main aspects of the system design. To deal with an ever growing complexity when designing for such heterogeneous and evolving platforms, software developers have to adopt a novel software design methodology that encourages the software customization through modularity, reuse and module assembly to build systems and applications. Component-based Software Engineering (CBSE), enabling software customization by adding, removing and substituting components seems to be adequate to reach that goal. We investigate this area while developing Think, a lightweight implementation of the Fractal component model, which applies CBSE principles down to the lowest software layer: the operating system. Think allows various kinds of communication semantics from simple method invocations to RPC, recursive component composition, and comes with retargetable configuration and specification tools. In this paper, we show how Think can make flexible and customizable the operating system and application design for MPSoC a reality. [ABSTRACT FROM AUTHOR]

System software for deeply embedded devices has to cope with a broad variety of requirements and platforms, but especially with strict resource constraints. To compete against proprietary systems (and thereby to facilitate reuse), an operating system product line for deeply embedded systems has to be highly configurable and tailorable. It is therefore crucial that all selectable and configurable features can be encapsulated into fine-grained, exchangeable and reusable implementation components. However, the encapsulation of non-functional properties is often limited, due to their cross-cutting character. Fundamental system policies, like synchronization or activation points for the scheduler, have typically to be reflected in many points of the operating system component code. The presented approach is based on feature modeling, C++ class composition and overcomes the above mentioned problems by means of aspect-oriented programming (AOP). It facilitates a fine-grained encapsulation and configuration of even non-functional properties in system software. [ABSTRACT FROM AUTHOR]

Much recent work on proof-carrying code aims to build certifying compilers for single-inheritance object-oriented languages, such as Java or C#. Some modern object-oriented languages support compiling a derived class without complete information about its base class. This strategy—though necessary for supporting features such as mixins, traits, and first-class classes—is not well-supported by existing typed intermediate languages. We present a low-level IL with a type system based on the Calculus of Inductive Constructions. It is an appropriate target for efficient, type-preserving compilation of various forms of inheritance, even when the base class is unknown at compile time. Languages (such as Java) that do not require such flexibility are not penalized at run time. [ABSTRACT FROM AUTHOR]

Memory is one of the scarcest resource of embedded and constrained devices. This paper studies the memory footprint benefit of pre-deploying embedded Java systems up to their activation using romization. We find out that the more the system is deployed off-board, the more it can be efficiently and automatically customized in order to reduce its final size. This claim is validated experimentally through the production of memory images that are between 10% and 45% the size of their J2ME CLDC counterparts, while using the J2SE API and being ready-to-run without any further on-board initialization. Embedded solutions like J2ME degrade the Java environment and API right from their specification, limiting their usage perspectives. By contrast, our romization scheme generates and specializes a custom-tailored Java API for embedded applications deployed in a full-fledged J2SE environment. [ABSTRACT FROM AUTHOR]

We study secure information flow in a stack based Typed Assembly Language (TAL). We define a TAL with an execution stack and establish the soundness of its type system by proving non-interference. One of the problems of studying information flow for a low-level language is the absence of high-level control flow constructs that guide information flow analysis in high-level languages. Furthermore, in the presence of an execution stack, code that frees space on the stack must be constrained in order to avoid illegal flows. Finally, in the presence of stack polymorphism, we must ensure that type variables are instantiated without observable differences. These issues are addressed by introducing junction points into the type system, ensuring that they behave as ordered linear continuations, and that they interact safely with the execution stack. We also discuss several limitations of our approach and point out some remaining open issues. [ABSTRACT FROM AUTHOR]

This paper introduces notions of resource policy for mobile code to be run on smart devices, to integrate with the proof-carrying code architecture of the Mobile Resource Guarantees (MRG) project. Two forms of policy are used: guaranteed policies which come with proofs and target policies which describe limits of the device. A guaranteed policy is expressed as a function of a methods input sizes, which determines a bound on consumption of some resource. A target policy is defined by a constant bound and input constraints for a method. A recipient of mobile code chooses whether to run methods by comparing between a guaranteed policy and the target policy. Since delivered code may use methods implemented on the target machine, guaranteed policies may also be provided by the platform; they appear symbolically as assumptions in delivered proofs. Guaranteed policies entail proof obligations that must be established from the proof certificate. Before proof, a policy checker ensures that the guaranteed policy refines the target policy; our policy format ensures that this step is tractable and does not require proof. Delivering policies thus mediates between arbitrary target requirements and the desirability to package code and certificate only once. [ABSTRACT FROM AUTHOR]

Today many interactions are carried out online through Web sites and e-services and often private and/or sensitive information is required by service providers. A growing concern related to this widespread diffusion of on-line applications that collect personal information is that users' privacy is often poorly managed and sometimes abused. For instance, it is well known how personal information is often disclosed to third parties without the consent of legitimate data owners or that there are professional services specialized on gathering and correlating data from heterogeneous repositories, which permit to build user profiles and possibly to disclose sensitive information not voluntarily released by their owners. For these reasons, it has gained great importance to design systems able to fully preserve information privacy by managing in a trustworthy and responsible way all identity and profile information. In this paper, we investigate some problems concerning identity management for e-services and present the architecture of the Access Control Decision Function, a software component in charge of managing access request in a privacy-aware fashion. The content of this paper is a result of our ongoing activity in the framework of the PRIME project (Privacy and Identity Management for Europe) [18], funded by the European Commission, whose objective is the development of privacy-aware solutions for enforcing security. [ABSTRACT FROM AUTHOR]

Pocklington certificates are known to provide short proofs of primality. We show how to perform this in the framework of formal, mechanically checked, proofs. We present an encoding of certificates for the proof system Coq which yields radically improved performances by relying heavily on computations inside and outside of the system (two-level approach). [ABSTRACT FROM AUTHOR]

This paper reports on the correctness proof of compiler optimizations based on data-flow analysis. We formulate the optimizations and analyses as instances of a general framework for data-flow analyses and transformations, and prove that the optimizations preserve the behavior of the compiled programs. This development is a part of a larger effort of certifying an optimizing compiler by proving semantic equivalence between source and compiled code. [ABSTRACT FROM AUTHOR]

Sized types provides a type-based mechanism to enforce termination of recursive definitions in typed λ-calculi. Previous work has provided strong indications that type-based termination provides an appropriate foundation for proof assistants based on type theory; however, most work to date has been confined to non-dependent type systems. In this article, we introduce a variant of the Calculus of Inductive Constructions with sized types and study its meta theoretical properties: subject reduction, normalization, and thus consistency and decidability of type-checking and of size-inference. A prototype implementation has been developed alongside case studies. [ABSTRACT FROM AUTHOR]

Computing efficiently with numbers can be crucial for some theorem proving applications. In this paper, we present a library of modular arithmetic that has been developed within the Coq proof assistant. The library proposes the usual operations that have all been proved correct. The library is purely functional but can also be used on top of some native modular arithmetic. With this library, we have been capable of certifying the primality of numbers with more than 13000 digits. [ABSTRACT FROM AUTHOR]

Certifying compilation provides a means to ensure that untrusted mobile code satisfies its functional specification. A certifying compiler generates code as well as a machine-checkable "certificate", i.e. a formal proof that establishes adherence of the code to specified properties. While certificates for safety properties can be built fully automatically, certificates for more expressive and complex properties often require the use of interactive code verification. We propose a technique to provide code consumers with the benefits of interactive source code verification. Our technique, certificate translation, extends program transformations by offering the means to turn certificates of functional correctness for programs in high-level languages into certificates for executable code. The article outlines the principles of certificate translation, using specifications written in first order logic. This translation is instantiated for standard compiler optimizations in the context of an intermediate RTL Language. [ABSTRACT FROM AUTHOR]

In proof systems like Coq [16], proof-checking involves comparing types modulo β-conversion, which is potentially a time-consuming task. Significant speed-ups are achieved by compiling proof terms, see [9]. Since compilation erases some type information, we have to show that convertibility is preserved by type erasure. This article shows the equivalence of the Calculus of Inductive Constructions (formalism of Coq) and its domain-free version where parameters of inductive types are also erased. It generalizes and strengthens significantly a similar result by Barthe and Sørensen [5] on the class of functional Domain-free Pure Type Systems. [ABSTRACT FROM AUTHOR]

We present a new implementation of a reflexive tactic which solves equalities in a ring structure inside the Coq system. The efficiency is improved to a point that we can now prove equalities that were previously beyond reach. A special care has been taken to implement efficient algorithms while keeping the complexity of the correctness proofs low. This leads to a single tool, with a single implementation, which can be addressed for a ring or for a semi-ring, abstract or not, using the Leibniz equality or a setoid equality. This example shows that such reflective methods can be effectively used in symbolic computation. [ABSTRACT FROM AUTHOR]

We introduce a polymorphic λ-calculus that features inductive types and that enforces termination of recursive definitions through typing. Then, we define a sound and complete type inference algorithm that computes a set of constraints to be satisfied for terms to be typable. In addition, we show that Subject Reduction fails in a naive use of typed-based termination for a λ-calculus à la Church, and we propose a general solution to this problem. [ABSTRACT FROM AUTHOR]