Search

We present a formally verified renaming refactoring for a subset of Haskell 98 giving a case-study in proving soundness properties of Haskell refactorings. Our renaming is implemented in the dependently- typed language Idris, which allows us to encode soundness proofs as an integral part of the implementation. We give the formal definition of our static semantics for our Haskell 98 subset, which we encode as part of the AST, ensuring that only well-formed programs may be represented and transformed. This forms a foundation upon which refactorings can be formally specified. We then define soundness of refactoring implementations as conformity to their specification. We demonstrate our approach via renaming, a canonical and well-understood refactoring, giving its implementation alongside its formal specification and soundness proof. Postprint

A trusted execution environment (TEE) such as Intel Software Guard Extension (SGX) runs attestation to prove to a data owner the integrity of the initial state of an enclave, including the program to operate on her data. For this purpose, the data-processing program is supposed to be open to the owner or a trusted third party, so its functionality can be evaluated before trust being established. In the real world, however, increasingly there are application scenarios in which the program itself needs to be protected (e.g., proprietary algorithm). So its compliance with privacy policies as expected by the data owner should be verified without exposing its code. To this end, this paper presents Deflection, a new model for TEE-based delegated and flexible in-enclave code verification. Given that the conventional solutions do not work well under the resource-limited and TCB-frugal TEE, we come up with a new design inspired by Proof-Carrying Code. Our design strategically moves most of the workload to the code generator, which is responsible for producing easy-to-check code, while keeping the consumer simple. Also, the whole consumer can be made public and verified through a conventional attestation. We implemented this model on Intel SGX and demonstrate that it introduces a very small part of TCB. We also thoroughly evaluated its performance on micro- and macro- benchmarks and real-world applications, showing that the design only incurs a small overhead when enforcing several categories of security policies.

Funding: EU Horizon 2020 project, TeamPlay (https://www.teamplay-h2020.eu), grant number 779882; UK EPSRC Discovery, grant number EP/P020631/1. Systems with non-functional requirements, such as Energy, Time and Security (ETS), are of increasing importance due to the proliferation of embedded devices with limited resources such as drones, wireless sensors, and tablet computers. Currently, however, there are little to no programmer supported methodologies or frameworks to allow them to reason about ETS properties in their source code. Drive is one such existing framework supporting the developer by lifting non-functional properties to the source-level through the Contract Specification Language (CSL), allowing non-functional properties to be first-class citizens, and supporting programmer-written code-level contracts to guarantee the non-functional specifications of the program are met. In this paper, we extend the Drive system by providing rigorous implementations of the underlying proof-engine, modeling the specification of the annotations and assertions from CSL for a representative subset of C, called Imp. We define both an improved abstract interpretation that automatically derives proofs of assertions, and define inference algorithms for the derivation of both abstract interpretations and the context over which the interpretation is indexed. We use the dependently-typed programming language, Idris, to give a formal definition, and implementation, of our abstract interpretation. Finally, we show our well-formed abstract interpretation over some representative exemplars demonstrating provable assertions of ETS. Postprint

The traditional static measurement method based on data integrity measurement can only prove that the software has not been tampered with, and cannot describe the software behavior status. Dynamic measurement can measure the software behavior in real time, but there is no doubt that it requires a lot of computing resources. In this paper, we propose static measurement architecture PMA, which using formal method to abstract and verify software behavior. In PMA, formal language abstracts software behavior, formal specification describes security policy, and software behavior measurement problem is transformed into formal proof. We also have implemented the corresponding code according to the PMA design principle. The experimental test verifies the feasibility of the PMA architecture.

A major design concern in modern software development frameworks is to ensure that mechanisms for updating code running on remote devices comply with given safety specifications. This paper presents a delta-oriented approach for implementing product lines where software reuse is achieved at the three levels of state-diagram modeling, C/ $$\text {C}^{_{_{_{++}}}} $$ source code and binary code. A safety specification is expressed on the properties of reusable software libraries that can be dynamically loaded at run time after an over-the-air update. The compilation of delta-engineered code is certified using the framework of proof-carrying code in order to guarantee safety of software updates on remote devices. An empirical evaluation of the computational cost associated with formal safety checks is done by means of experimentation.

Today, software is traded worldwide on global markets, with apps being downloaded to smartphones within minutes or seconds. This poses, more than ever, the challenge of ensuring safety of software in the face of (1) unknown or untrusted software providers together with (2) resource-limited software consumers. The concept of Proof-Carrying Code (PCC), years ago suggested by Necula, provides one framework for securing the execution of untrusted code. PCC techniques attach safety proofs, constructed by software producers, to code. Based on the assumption that checking proofs is usually much simpler than constructing proofs, software consumers should thus be able to quickly check the safety of software. However, PCC techniques often suffer from the size of certificates (i.e., the attached proofs), making PCC techniques inefficient in practice. In this article, we introduce a new framework for the safe execution of untrusted code called Programs from Proofs (PfP). The basic assumption underlying the PfP technique is the fact that the structure of programs significantly influences the complexity of checking a specific safety property. Instead of attaching proofs to program code, the PfP technique transforms the program into an efficiently checkable form, thus guaranteeing quick safety checks for software consumers. For this transformation, the technique also uses a producer-side automatic proof of safety. More specifically, safety proving for the software producer proceeds via the construction of an abstract reachability graph (ARG) unfolding the control-flow automaton (CFA) up to the degree necessary for simple checking. To this end, we combine different sorts of software analysis: expensive analyses incrementally determining the degree of unfolding, and cheap analyses responsible for safety checking. Out of the abstract reachability graph we generate the new program. In its CFA structure, it is isomorphic to the graph and hence another, this time consumer-side, cheap analysis can quickly determine its safety. Like PCC, Programs from Proofs is a general framework instantiable with different sorts of (expensive and cheap) analysis. Here, we present the general framework and exemplify it by some concrete examples. We have implemented different instantiations on top of the configurable program analysis tool CPA checker and report on experiments, in particular on comparisons with PCC techniques.

International audience; The work presented in this paper lies in the context of implementing supporting tools for a domain-specific language named SosADL, targeted at the description and analysis of architecture for systems of systems. While the language has formal definition rooted in the Cc-pi calculus, we have adopted the Eclipse ecosystem, including EMF, Ecore and Xtext for the convenience they provide in implementation tasks. Proof-carrying code is a well-known approach to ensure such an implementation involving non-formal technologies conforms to its formal definition, by making the implementation generate proof in addition to usual output artifacts. In this paper, we therefore investigate for an infrastructure that eases the development of proof-carrying code for an Eclipse/EMF/Ecore/Xtext-based tool in relation with the Coq proof assistant. At the core of our approach, we combine an automatic transformation of a metamodel into a set of inductive types, in conjunction with a second transformation of model elements into terms. The first one, reused from our previous work, provides necessary abstract syntax definitions such that the formal definition of the language can be mechanized using Coq. The second transformation is part of the proof generator.

Systems with non-functional requirements, such as Energy, Time and Security (ETS), are of increasing importance due to the proliferation of embedded devices with limited resources such as drones, wireless sensors, and tablet computers. Currently, however, there are little to no programmer supported methodologies or frameworks to allow them to reason about ETS properties in their source code. Drive is one such existing framework supporting the developer by lifting non-functional properties to the source-level through the Contract Specification Language (CSL), allowing non-functional properties to be first-class citizens, and supporting programmer-written code-level contracts to guarantee the non-functional specifications of the program are met. In this paper, we extend the Drive system by providing rigorous implementations of the underlying proof-engine, modeling the specification of the annotations and assertions from CSL for a representative subset of C, called Imp. We define both an improved abstract interpretation that automatically derives proofs of assertions, and define inference algorithms for the derivation of both abstract interpretations and the context over which the interpretation is indexed. We use the dependently-typed programming language, Idris, to give a formal definition, and implementation, of our abstract interpretation. Finally, we show our well-formed abstract interpretation over some representative exemplars demonstrating provable assertions of ETS.

The work presented in this paper lies in the context of implementing supporting tools for a domain-specific language named SosADL, targeted at the description and analysis of architecture for systems of systems. While the language has formal definition rooted in the Cc-pi calculus, we have adopted the Eclipse ecosystem, including EMF, Ecore and Xtext for the convenience they provide in implementation tasks. Proof-carrying code is a well-known approach to ensure such an implementation involving non-formal technologies conforms to its formal definition, by making the implementation generate proof in addition to usual output artifacts. In this paper, we therefore investigate for an infrastructure that eases the development of proof-carrying code for an Eclipse/EMF/Ecore/Xtext-based tool in relation with the Coq proof assistant. At the core of our approach, we combine an automatic transformation of a metamodel into a set of inductive types, in conjunction with a second transformation of model elements into terms. The first one, reused from our previous work, provides necessary abstract syntax definitions such that the formal definition of the language can be mechanized using Coq. The second transformation is part of the proof generator. 64 259 273

Injection attacks top the lists of the most harmful software vulnerabilities. Injection vulnerabilities are both commonplace and easy to exploit, which makes development of injection protection schemes important. In this article, we show how injection attacks can be practically eliminated through the use of structured data paired with cryptographic verification codes upon transmission. peerReviewed

Information flow analysis investigates the flow of data in applications, checking in particular for flows from private sources to public sinks. Flow- and path-sensitive analyses are, however, often too costly to be performed every time a security-critical application is run. In this paper, we propose a variant of proof carrying code for information flow security. To this end, we develop information flow (IF) certificates which get attached to programs as well as a method for IF certificate validation. We prove soundness of our technique, i.e., show it to be tamper-free. The technique is implemented within the program analysis tool CPAchecker. Our experiments confirm that the use of certificates pays off for costly analysis runs.

In this paper we summarise Safe, a first-order functional language for programming small devices and embedded systems with strict memory requirements, which has been introduced elsewhere. It has some unusual memory management features such as heap regions and explicit cell deallocation. It is targeted at a Proof Carrying Code environment, and consistently with this aim the Safe compiler provides machine checkable certificates about important safety properties such as the absence of dangling pointers and bounded memory consumption. The kernel of the paper is devoted to developing part of the Safe compiler's back-end, by deriving an appropriate abstract machine from the language semantics, by providing the code generation functions, and by formally proving that the translation is sound, both in the semantic and in the memory consumption senses.

Buffer overflow has been one of the most outstanding attacks in the last ten years. This kind of vulnerability may compromise the system security by various means. Existing solutions to this problem have focused on the execution environment of the malicious program rather than the hypostasis of buffer overflow and most of them try to detect buffer overflows dynamically. This paper presents the effort of applying a static analysis approach against the programs exploiting buffer overflow and the method adopted is named Proof-Carrying Code (PCC). This paper shows that: (1) it is possible to defend against most of the buffer overflow vulnerabilities with proper use of PCC; and (2) the method is well prepared to handle the coming-up variants of the buffer overflow problems. 

International audience; Implicit Computational Complexity (ICC) aims atgiving machine-free characterisations of complexity classes. Be-cause it is usually sound but not complete, it actually providescertificates that a given program can be run within a givenamount of resources. ICC is usually applied on toy languages withrestricted expressivity, we show here that it can be performed onreal programming languages.Because it is usually a static, syntactical analysis of theprograms, ICC is well-suited to be performed at compile time.The bounds given by ICC can then be used to fuel someoptimisation or to produce certificates of good behaviour. Moderncompilers do most of their work in a modular sequences of passesdone on some Intermediate Representation (IR) language. TheIR is a generic typed assembly-like language and thus very wellsuited to express ICC criteria. The modularity of the passes makeit easy to add one and to re-use existing ones at will.We focus here on the relatively simple analysis of Non-SizeIncreasing (NSI) programs. We’ve implemented a NSI analysisfor the LLVM compiler. This can be seen as a proof of conceptthat ICC and compilers are able to interact productively.

A certificate is a mathematical object that can be used to establish that a piece of mobile code satisfies some security policy. In general, certificates cannot be generated automatically. There is thus an interest in developing methods to reuse certificates generated for source code to provide strong guarantees of the compiled code correctness. Certificate translation is a method to transform certificates of program correctness along semantically justified program transformations. These methods have been developed in previous work, but they were strongly dependent on particular programming and verification settings. This article provides a more general development in the setting of abstract interpretation, showing the scalability of certificate translation.

Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably expressive logic plus a specification of machine semantics. This article proposes general semantic foundations that permit modular proofs of the soundness of TALs. These semantic foundations include Typed Machine Language (TML), a type theory for specifying properties of low-level data with powerful and orthogonal type constructors, and L c , a compositional logic for specifying properties of machine instructions with simplified reasoning about unstructured control flow. Both of these components, whose semantics we specify using higher-order logic, are useful for proving the soundness of TALs. We demonstrate this by using TML and L c to verify the soundness of a low-level, typed assembly language, LTAL, which is the target of our core-ML-to-sparc compiler. To prove the soundness of the TML type system we have successfully applied a new approach, that of step-indexed logical relations . This approach provides the first semantic model for a type system with updatable references to values of impredicative quantified types. Both impredicative polymorphism and mutable references are essential when representing function closures in compilers with typed closure conversion, or when compiling objects to simpler typed primitives.

Proof Carrying Code provides trust in mobile code by requiring certificates that ensure the code adherence to specific conditions. The prominent approach to generate certificates for compiled code is Certifying Compilation, that automatically generates certificates for simple safety properties. In this work, we present Certificate Translation, a novel extension for standard compilers that automatically transforms formal proofs for more expressive and complex properties of the source program to certificates for the compiled code. The article outlines the principles of certificate translation, instantiated for a nonoptimizing compiler and for standard compiler optimizations in the context of an intermediate RTL Language.

Runtime monitoring is an established technique to enforce a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has a copy of the given monitor embedded into it. As the main application of these results we sketch a simple inlining algorithm and show how the two-level annotations can be completed to produce a fully annotated program which is valid in the standard sense of Floyd/Hoare logic. This establishes the mediation property that inlined programs are guaranteed to adhere to the intended policy. Furthermore, validity can be checked efficiently using a weakest precondition based annotation checker, thus preparing the ground for on-device checking of policy adherence in a proof-carrying code setting.