Programming Languages and Systems

Frontmatter

Programming with Explicit Security Policies

Abstract

Are computing systems trustworthy? To answer this, we need to know three things: what the systems are supposed to do, what they are not supposed to do, and what they actually do. All three are problematic. There is no expressive, practical way to specify what systems must do and must not do. And if we had a specification, it would likely be infeasible to show that existing computing systems satisfy it. The alternative is to design it in from the beginning: accompany programs with explicit, machine-checked security policies, written by programmers as part of program development. Trustworthy systems must safeguard the end-to-end confidentiality, integrity, and availability of information they manipulate. We currently lack both sufficiently expressive specifications for these information security properties, and sufficiently accurate methods for checking them. Fortunately there has been progress on both fronts. First, information security policies can be made more expressive than simple noninterference or access control policies, by adding notions of ownership, declassification, robustness, and erasure. Second, program analysis and transformation can be used to provide strong, automated security assurance, yielding a kind of security by construction. This is an overview of programming with explicit information security policies with an outline of some future challenges.

Andrew C. Myers

Trace Partitioning in Abstract Interpretation Based Static Analyzers

Abstract

When designing a tractable static analysis, one usually needs to approximate the trace semantics. This paper proposes a systematic way of regaining some knowledge about the traces by performing the abstraction over a partition of the set of traces instead of the set itself. This systematic refinement is not only theoretical but tractable: we give automatic procedures to build pertinent partitions of the traces and show the efficiency on an implementation integrated in the Astrée static analyzer, a tool capable of dealing with industrial-size software.

Laurent Mauborgne, Xavier Rival

The ASTREÉ Analyzer

Abstract

ASTRÉE is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C programming language. It has been applied with success to large embedded control-command safety critical real-time software generated automatically from synchronous specifications, producing a correctness proof for complex software without any false alarm in a few hours of computation.

Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival

Interprocedural Herbrand Equalities

Abstract

We present an aggressive interprocedural analysis for inferring value equalities which are independent of the concrete interpretation of the operator symbols. These equalities, called Herbrand equalities, are therefore an ideal basis for truly machine-independent optimizations as they hold on every machine. Besides a general correctness theorem, covering arbitrary call-by-value parameters and local and global variables, we also obtain two new completeness results: one by constraining the analysis problem to Herbrand constants, and one by allowing side-effect-free functions only. Thus if we miss a constant/equality in these two scenarios, then there exists a separating interpretation of the operator symbols.

Markus Müller-Olm, Helmut Seidl, Bernhard Steffen

Analysis of Modular Arithmetic

Abstract

We consider integer arithmetic modulo a power of 2 as provided by mainstream programming languages like Java or standard implementations of C. The difficulty here is that the ring ℤ _m of integers modulo m = 2 ^w , w > 1, has zero divisors and thus cannot be embedded into a field. Not withstanding that, we present intra- and inter-procedural algorithms for inferring for every program point u, affine relations between program variables valid at u. Our algorithms are not only sound but also complete in that they detect all valid affine relations. Moreover, they run in time linear in the program size and polynomial in the number of program variables and can be implemented by using the same modular integer arithmetic as the target language to be analyzed.

Markus Müller-Olm, Helmut Seidl

Forward Slicing by Conjunctive Partial Deduction and Argument Filtering

Abstract

Program slicing is a well-known methodology that aims at identifying the program statements that (potentially) affect the values computed at some point of interest. Within imperative programming, this technique has been successfully applied to debugging, specialization, reuse, maintenance, etc. Due to its declarative nature, adapting the slicing notions and techniques to a logic programming setting is not an easy task. In this work, we define the first, semantics-preserving, forward slicing technique for logic programs. Our approach relies on the application of a conjunctive partial deduction algorithm for a precise propagation of information between calls. We do not distinguish between static and dynamic slicing since partial deduction can naturally deal with both static and dynamic data. A slicing tool has been implemented in ecce, where a post-processing transformation to remove redundant arguments has been added. Experiments conducted on a wide variety of programs are encouraging and demonstrate the usefulness of our approach, both as a classical slicing method and as a technique for code size reduction.

Michael Leuschel, Germán Vidal

A New Foundation for Control-Dependence and Slicing for Modern Program Structures

Abstract

The notion of control dependence underlies many program analysis and transformation techniques. Despite wide applications, existing definitions and approaches for calculating control dependence are difficult to apply seamlessly to modern program structures. Such program structures make substantial use of exception processing and increasingly support reactive systems designed to run indefinitely.

This paper revisits foundational issues surrounding control dependence and slicing. It develops definitions and algorithms for computing control dependence that can be directly applied to modern program structures. A variety of properties show that the new definitions conservatively extend classic definitions. In the context of slicing reactive systems, the paper proposes a notion of slicing correctness based on weak bisimulation and proves that the definition of control dependence generates slices that conform to this notion of correctness. The new definitions and algorithms for control dependence form the basis of a publicly available program slicer that has been implemented for full Java.

Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer, John Hatcliff

Summaries for While Programs with Recursion

Abstract

Procedure summaries are an approximation of the effect of a procedure call. They have been used to prove partial correctness and safety properties. In this paper, we introduce a generalized notion of procedure summaries and present a framework to verify total correctness and liveness properties of a general class of while programs with recursion. We provide a fixpoint system for computing summaries, and a proof rule for total correctness of a program given a summary. With suitable abstraction methods and algorithms for efficient summary computation, the results presented here can be used for the automatic verification of termination and liveness properties for while programs with recursion.

Andreas Podelski, Ina Schaefer, Silke Wagner

Determinacy Inference for Logic Programs

Abstract

This paper presents a determinacy inference analysis for logic programs. The analysis infers determinacy conditions that, if satisfied by a call, ensures that it computes at most one answer and that answer is generated only once. The principal component of the technique is a goal-independent analysis of individual clauses. This derives a condition for a call that ensures only one clause in the matching predicate possesses a successful derivation. Another key component of the analysis is backwards reasoning stage that strengthens these conditions to derive properties on a call that assure determinacy. The analysis has applications in program development, implementation and specialisation.

Lunjin Lu, Andy King

Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis

Abstract

We present a program analysis that can automatically discover the shape of complex pointer data structures. The discovered invariants are, then, used to verify the absence of safety errors in the program, or to check whether the program preserves the data consistency. Our analysis extends the shape analysis of Sagiv et al. with grammar annotations, which can precisely express the shape of complex data structures. We demonstrate the usefulness of our analysis with binomial heap construction and the Schorr-Waite tree traversal. For a binomial heap construction algorithm, our analysis returns a grammar that precisely describes the shape of a binomial heap; for the Schorr-Waite tree traversal, our analysis shows that at the end of the execution, the result is a tree and there are no memory leaks.

Oukseh Lee, Hongseok Yang, Kwangkeun Yi

A Type Discipline for Authorization Policies

Abstract

Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as, for instance, digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs, in particular, can express policies in a simple, abstract manner.

For a given authorization policy, we consider the problem of checking whether a cryptographic implementation complies with the policy. We formalize authorization policies by embedding logical predicates and queries within a spi calculus. This embedding is new, simple, and general; it allows us to treat logic programs as specifications of code using secure channels, cryptography, or a combination. Moreover, we propose a new dependent type system for verifying such implementations against their policies. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.

Cédric Fournet, Andrew D. Gordon, Sergio Maffeis

Computationally Sound, Automated Proofs for Security Protocols

Abstract

Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers have been quite unclear.

In this paper, we show that it is possible to obtain the best of both worlds: fully automated proofs and strong, clear security guarantees. Specifically, for the case of protocols that use signatures and asymmetric encryption, we establish that symbolic integrity and secrecy proofs are sound with respect to the computational model. The main new challenges concern secrecy properties for which we obtain the first soundness result for the case of active adversaries. Our proofs are carried out using Casrul, a fully automated tool.

Véronique Cortier, Bogdan Warinschi

Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries

Abstract

In this paper, we extend previous results relating the Dolev-Yao model and the computational model. We add the possibility to exchange keys and consider cryptographic primitives such as signature. This work can be applied to check protocols in the computational model by using automatic verification tools in the formal model.

To obtain this result, we introduce a precise definition for security criteria which leads to a nice reduction theorem. The reduction theorem is of interest on its own as it seems to be a powerful tool for proving equivalences between security criteria. Also, the proof of this theorem uses original ideas that seem to be applicable in other situations.

Romain Janvier, Yassine Lakhnech, Laurent Mazaré

Analysis of an Electronic Voting Protocol in the Applied Pi Calculus

Abstract

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. The applied pi calculus is a formalism for modelling such protocols, and allows us to verify properties by using automatic tools, and to rely on manual proof techniques for cases that automatic tools are unable to handle. We model a known protocol for elections known as FOO 92 in the applied pi calculus, and we formalise three of its expected properties, namely fairness, eligibility, and privacy. We use the ProVerif tool to prove that the first two properties are satisfied. In the case of the third property, ProVerif is unable to prove it directly, because its ability to prove observational equivalence between processes is not complete. We provide a manual proof of the required equivalence.

Steve Kremer, Mark Ryan

Streams with a Bottom in Functional Languages

Abstract

When an infinite sequence contains a bottom cell, we cannot access the rest of the sequence with the ordinary stream access. On the other hand, when we consider an extended stream access with two heads, we can read or write 1\(\bot\)-sequences, which are infinite sequences with at most one bottom cell. In this paper, we present a way of extending a lazy functional language with such an extended stream access in the realm of sequential computation. It has an application in real number computation in that the set of real numbers is topologically embedded in the set of 1 \(\bot\)-sequences [16], and therefore we can consider a program with such an extended stream access as directly manipulating real numbers. We implemented this mechanism by modifying the runtime of the Hugs system, which is a graph-reduction based implementation of the Haskell language. We present programming examples like addition and multiplication on real numbers in this extended Haskell.

For this implementation, we extended Haskell with the gamb operator, which works just as McCarthy’s bottom-avoiding nondeterministic choice operator “amb”. The difference is that it is realized in the realm of sequential computation, and that it is applicable only when the graph representations of the arguments share the same redex. In order to show that programs corresponding to two-head stream accesses satisfy this condition, we introduce a PCF-based calculus of term-graphs and define a data-type of 1 \(\bot\)-streams as a subtype of [Bool].

Hideki Tsuiki, Keiji Sugihara

Bottom-Up β-Reduction: Uplinks and λ-DAGs

Abstract

Representing a λ term as a DAG rather than a tree allows us to represent the sharing that arises from β, thus avoiding combinatorial explosion in space. By adding uplinks from a child to its parents, we can efficiently implement β in a bottom-up manner, thus avoiding combinatorial explosion in time required to search the term in a top-down fashion. We present an algorithm for performing β onλ-terms represented as uplinked DAGs; discuss its relation to alternate techniques such as Lamping graphs, explicit-substitution calculi and director strings; and present some timings of an implementation. Besides being both fast and parsimonious of space, the algorithm is particularly suited to applications such as compilers, theorem provers, and type-manipulation systems that may need to examine terms in-between reductions—i.e., the “readback” problem for our representation is trivial. Like Lamping graphs, and unlike director strings or the suspension λ, the algorithm functions by side-effecting the term containing the redex; the representation is not a “persistent” one. The algorithm additionally has the charm of being quite simple: a complete implementation of the core data structures and algorithms is 180 lines of SML.

Olin Shivers, Mitchell Wand

BI Hyperdoctrines and Higher-Order Separation Logic

Abstract

We present a precise correspondence between separation logic and a new simple notion of predicate BI, extending the earlier correspondence given between part of separation logic and propositional BI [14]. Moreover, we introduce the notion of a BI hyperdoctrine and show that it soundly models classical and intuitionistic first- and higher-order predicate BI, and use it to show that we may easily extend separation logic to higher-order. We argue that the given correspondence may be of import for formalizations of separation logic.

Bodil Biering, Lars Birkedal, Noah Torp-Smith

Deciding Reachability in Mobile Ambients

Abstract

Mobile Ambients has been proposed by Cardelli and Gordon as a foundational calculus for mobile computing. Since its introduction, the computational strength as well as the decidability of properties have been investigated for several fragments and variants of the standard calculus. We tackle the problem of reachability and we characterize a public (i.e., restriction free) fragment for which it is decidable. This fragment is obtained by removing the open capability and restricting the use of replication to guarded processes. Quite surprisingly, this fragment has been shown to be Turing complete by Maffeis and Phillips.

Nadia Busi, Gianluigi Zavattaro

Denotational Semantics for Abadi and Leino’s Logic of Objects

Abstract

Abadi-Leino Logic is a Hoare-calculus style logic for a simple imperative and object-based language where every object comes with its own method suite. Consequently, methods need to reside in the store (”higher-order store”). We present a new soundness proof for this logic using a denotational semantics where object specifications are recursive predicates on the domain of objects. Our semantics reveals which of the limitations of Abadi and Leino’s logic are deliberate design decisions and which follow from the use of higher-order store. We discuss the implications for the development of other, more expressive, program logics.

Bernhard Reus, Jan Schwinghammer

A Design for a Security-Typed Language with Certificate-Based Declassification

Abstract

This paper presents a calculus that supports information-flow security policies and certificate-based declassification. The decentralized label model and its downgrading mechanisms are concisely expressed in the polymorphic lambda calculus with subtyping (System F _≽). We prove a conditioned version of the noninterference theorem such that authorization for declassification is justified by digital certificates from public-key infrastructures.

Stephen Tse, Steve Zdancewic

Adjoining Declassification and Attack Models by Abstract Interpretation

Abstract

In this paper we prove that attack models and robust declassification in language-based security can be viewed as adjoint transformations of abstract interpretations. This is achieved by interpreting the well known Joshi and Leino’s semantic approach to non-interference as a problem of making an abstraction complete relatively to a program’s semantics. This observation allows us to prove that the most abstract property on confidential data which flows, here called private observation, and the most concrete harmless attacker observing public data, here called public observable, both modeled as abstractions of the program’s semantics, are respectively the adjoint solutions of a completeness problem in standard abstract interpretation theory. In particular declassification corresponds to refining the given model of an attacker with the minimal amount of information in order to achieve completeness, which is non-interference, while the harmless attacker corresponds to remove this information. This proves an adjunction relation between two basic approaches to language-based security: declassification and the construction of suitable attack models, and allows us to apply relevant techniques for abstract domain transformation in language-based security.

Roberto Giacobazzi, Isabella Mastroeni

Enforcing Resource Bounds via Static Verification of Dynamic Checks

Abstract

We classify existing approaches to resource-bounds checking as static or dynamic. Dynamic checking performs checks during program execution, while static checking performs them before execution. Dynamic checking is easy to implement but incurs runtime cost. Static checking avoids runtime overhead but typically involves difficult, often incomplete program analyses. In particular, static checking is hard in the presence of dynamic data and complex program structure. We propose a new resource management paradigm that offers the best of both worlds. We present language constructs that let the code producer optimize dynamic checks by placing them either before each resource use, or at the start of the program, or anywhere in between. We show how the code consumer can then statically verify that the optimized dynamic checks enforce his resource bounds policy. We present a practical language that is designed to admit decidable yet efficient verification and prove that our procedure is sound and optimal. We describe our experience verifying a Java implementation of tar for resource safety. Finally, we outline how our method can improve the checking of other dynamic properties.

Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George Necula

Asserting Bytecode Safety

Abstract

We instantiate an Isabelle/HOL framework for proof carrying code to Jinja bytecode, a downsized variant of Java bytecode featuring objects, inheritance, method calls and exceptions. Bytecode annotated in a first order expression language can be certified not to produce arithmetic overflows. For this purpose we use a generic verification condition generator, which we have proven correct and relatively complete.

Martin Wildmoser, Tobias Nipkow

Subtyping First-Class Polymorphic Components

Abstract

We present a statically typed, class-based object oriented language where classes are first class polymorphic values. A main contribution of this work is the design of a type system that combines first class polymorphic values with structural equirecursive types and admits a subtyping algorithm which is arguably much simpler than existing alternatives. Our development is modular and can be easily instantiated for either a Kernel-Fun or a \(F_{\leq}^{\top}\) style of subtyping discipline.

João Costa Seco, Luís Caires

Complexity of Subtype Satisfiability over Posets

Abstract

Subtype satisfiability is an important problem for designing advanced subtype systems and subtype-based program analysis algorithms. The problem is well understood if the atomic types form a lattice. However, little is known about subtype satisfiability over posets. In this paper, we investigate algorithms for and the complexity of subtype satisfiability over general posets.We present a uniform treatment of different flavors of subtyping: simple versus recursive types and structural versus non-structural subtype orders.Our results are established through a new connection of subtype constraints and modal logic. As a consequence, we settle a problem left open by Tiuryn and Wand in 1993.

Joachim Niehren, Tim Priesnitz, Zhendong Su

A Type System Equivalent to a Model Checker

Abstract

Type systems and model checking are two prevalent approaches to program verification. A prominent difference between them is that type systems are typically defined in a syntactic and modular style whereas model checking is usually performed in a semantic and whole-program style. This difference between the two approaches lends them complementary to each other: type systems are good at explaining why a program was accepted while model checkers are good at explaining why a program was rejected.

We present a type system that is equivalent to a model checker for verifying temporal safety properties of imperative programs. The model checker is natural and may be instantiated with any finite-state abstraction scheme such as predicate abstraction. The type system which is also parametric type checks exactly those programs that are accepted by the model checker. It uses function types to capture flow sensitivity and intersection and union types to capture context sensitivity. Our result sheds light on the relationship between the two approaches, provides a methodology for studying their relative expressiveness, is a step towards sharing results between them, and motivates synergistic program analyses involving interplay between them.

Mayur Naik, Jens Palsberg

Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close

Abstract

Many different mobile process calculi have been invented, and for each some number of type systems has been developed. Soundness and other properties must be proved separately for each calculus and type system. We present the generic polymorphic type system Poly* which works for a wide range of mobile process calculi, including the π-calculus and Mobile Ambients. For any calculus satisfying some general syntactic conditions, well-formedness rules for types are derived automatically from the reduction rules and Poly* works otherwise unchanged. The derived type system is automatically sound (i.e., has subject reduction) and often more precise than previous type systems for the calculus, due to Poly*’s spatial polymorphism. We present an implemented type inference algorithm for Poly* which automatically constructs a typing given a set of reduction rules and a term to be typed. The generated typings are principal with respect to certain natural type shape constraints.

Henning Makholm, J. B. Wells

Towards a Type System for Analyzing JavaScript Programs

Abstract

JavaScript is a popular language for client-side web scripting. It has a dubious reputation among programmers for two reasons. First, many JavaScript programs are written against a rapidly evolving API whose implementations are sometimes contradictory and idiosyncratic. Second, the language is only weakly typed and comes virtually without development tools.

The present work is a first attempt to address the second point. It does so by defining a type system that tracks the possible traits of an object and flags suspicious type conversions. Because JavaScript is a classless, object-based language with first-class functions, the type system must include singleton types, subtyping, and first class record labels. The type system covers a representative subset of the language and there is a type soundness proof with respect to an operational semantics.

Peter Thiemann

Java JR: Fully Abstract Trace Semantics for a Core Java Language

Abstract

We introduce an expressive yet semantically clean core Java-like language, Java JR, and provide it with a formal operational semantics based on traces of observable actions which represent interaction across package boundaries. A detailed example based on the Observer Pattern is used to demonstrate the intuitive character of the semantic model. We also show that our semantic trace equivalence is fully-abstract with respect to a natural notion of testing equivalence for object systems. This is the first such result for a full class-based OO-language with inheritance.

Alan Jeffrey, Julian Rathke

Backmatter