Invited Contributions

Frontmatter

Programming by Examples: PL Meets ML

Abstract

Programming by Examples (PBE) involves synthesizing intended programs in an underlying domain-specific language from example-based specifications. PBE systems are already revolutionizing the application domain of data wrangling and are set to significantly impact several other domains including code refactoring.

There are three key components in a PBE system. (i) A search algorithm that can efficiently search for programs that are consistent with the examples provided by the user. We leverage a divide-and-conquer-based deductive search paradigm that inductively reduces the problem of synthesizing a program expression of a certain kind that satisfies a given specification into sub-problems that refer to sub-expressions or sub-specifications. (ii) Program ranking techniques to pick an intended program from among the many that satisfy the examples provided by the user. We leverage features of the program structure as well of the outputs generated by the program on test inputs. (iii) User interaction models to facilitate usability and debuggability. We leverage active-learning techniques based on clustering inputs and synthesizing multiple programs.

Each of these PBE components leverage both symbolic reasoning and heuristics. We make the case for synthesizing these heuristics from training data using appropriate machine learning methods. This can not only lead to better heuristics, but can also enable easier development, maintenance, and even personalization of a PBE system.

Sumit Gulwani, Prateek Jain

Synthesizing SystemC Code from Delay Hybrid CSP

Abstract

Delay is omnipresent in modern control systems, which can prompt oscillations and may cause deterioration of control performance, invalidate both stability and safety properties. This implies that safety or stability certificates obtained on idealized, delay-free models of systems prone to delayed coupling may be erratic, and further the incorrectness of the executable code generated from these models. However, automated methods for system verification and code generation that ought to address models of system dynamics reflecting delays have not been paid enough attention yet in the computer science community. In our previous work, on one hand, we investigated the verification of delay dynamical and hybrid systems; on the other hand, we also addressed how to synthesize SystemC code from a verified hybrid system modelled by Hybrid CSP (HCSP) without delay. In this paper, we give a first attempt to synthesize SystemC code from a verified delay hybrid system modelled by Delay HCSP (dHCSP), which is an extension of HCSP by replacing ordinary differential equations (ODEs) with delay differential equations (DDEs). We implement a tool to support the automatic translation from dHCSP to SystemC.

Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan

Security

Frontmatter

Taming Message-Passing Communication in Compositional Reasoning About Confidentiality

Abstract

We propose a solution for verifying the information-flow security of distributed programs in a compositional manner. Our focus is on the treatment of message passing in such a verification, and our goal is to boost the precision of modular reasoning using rely-guarantee-style reasoning. Enabling a more precise treatment of message passing required the identification of novel concepts that capture assumptions about how a process’s environment interacts. Our technical contributions include a process-local security condition that allows one to exploit such assumptions when analyzing individual processes, a security type system that is sensitive in the content as well as in the availability of messages, and a soundness proof for our security type system. Our results complement existing solutions for rely-guarantee-style reasoning about information-flow security that focused on multi-threading and shared memory.

Ximeng Li, Heiko Mantel, Markus Tasch

Capabilities for Java: Secure Access to Resources

Abstract

This paper explores adding capabilities to Java with the objective of tightening security management for access to resources both within the Java Class Library and Java applications. Code can only access resources if it is given explicit capabilities, allowing replacement of the use of doPrivileged blocks. Capabilities provide restricted access to their implementing object – like an interface – but when a capability is created, it has a more restrictive dynamic type than its implementing object, and hence access to the full facilities of the implementing object (e.g. via down casting) are precluded. We used the Annotation Processing Tool to track the declaration and use of capabilities.

Ian J. Hayes, Xi Wu, Larissa A. Meinicke

Enforcing Programming Guidelines with Region Types and Effects

Abstract

We present in this paper a new type and effect system for Java which can be used to ensure adherence to guidelines for secure web programming. The system is based on the region and effect system by Beringer, Grabowski, and Hofmann. It improves upon it by being parametrized over an arbitrary guideline supplied in the form of a finite monoid or automaton and a type annotation or mockup code for external methods. Furthermore, we add a powerful type inference based on precise interprocedural analysis and provide an implementation in the Soot framework which has been tested on a number of benchmarks including large parts of the Stanford SecuriBench.

Serdar Erbatur, Martin Hofmann, Eugen Zălinescu

Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications

Abstract

Intel Software Guard Extensions (SGX) is a recent technology from Intel that makes it possible to execute security-critical parts of an application in a so-called SGX enclave, an isolated area of the system that is shielded from all other software (including the OS and/or hypervisor). SGX was designed with the objective of making it relatively straightforward to take a single module of an existing C application, and put that module in an enclave. The SGX SDK includes tooling to semi-automatically generate wrappers for an enclaved C module. The wrapped enclave can then easily be linked to the legacy application that uses the module.

However, when the enclaved module and the surrounding application share a part of the heap and exchange pointers (a very common case in C programs), the generation of these wrappers requires programmer annotations and is error-prone – it is easy to introduce security vulnerabilities or program crashes.

This paper proposes a separation logic based language for specifying the interface of the enclaved C module, and shows how such an interface specification can be used to automatically generate secure wrappers that avoid these vulnerabilities and crashes.

Neline van Ginkel, Raoul Strackx, Frank Piessens

Heap and Equivalence Reasoning

Frontmatter

Black-Box Equivalence Checking Across Compiler Optimizations

Abstract

Equivalence checking is an important building block for program synthesis and verification. For a synthesis tool to compete with modern compilers, its equivalence checker should be able to verify the transformations produced by these compilers. We find that the transformations produced by compilers are much varied and the presence of undefined behaviour allows them to produce even more aggressive optimizations. Previous work on equivalence checking has been done in the context of translation validation, where either a pass-by-pass based approach was employed or a set of handpicked optimizations were proven. These settings are not suitable for a synthesis tool where a black-box approach is required.

This paper presents the design and implementation of an equivalence checker which can perform black-box checking across almost all the composed transformations produced by modern compilers. We evaluate the checker by testing it across unoptimized and optimized binaries of SPEC benchmarks generated by gcc, clang, icc and ccomp. The tool has overall success rates of 76% and 72% for O2 and O3 optimizations respectively, for this first of its kind experiment.

Manjeet Dahiya, Sorav Bansal

Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects

Abstract

JavaScript framework libraries like jQuery are widely used, but complicate program analyses. Indeed, they encode clean high-level constructions such as class inheritance via dynamic object copies and transformations that are harder to reason about. One common pattern used in them consists of loops that copy or transform part or all of the fields of an object. Such loops are challenging to analyze precisely, due to weak updates and as unrolling techniques do not always apply. In this paper, we observe that precise field correspondence relations are required for client analyses (e.g., for call-graph construction), and propose abstractions of objects and program executions that allow to reason separately about the effect of distinct iterations without resorting to full unrolling. We formalize and implement an analysis based on this technique. We assess the performance and precision on the computation of call-graph information on examples from jQuery tutorials.

Yoonseok Ko, Xavier Rival, Sukyoung Ryu

Decision Procedure for Entailment of Symbolic Heaps with Arrays

Abstract

This paper gives a decision procedure for the validity of entailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially bound. This condition is independent of the condition proposed by the CADE-2017 paper by Brotherston et al., namely, one of them does not imply the other. For improving efficiency of the decision procedure, some techniques are also presented. The main idea of the decision procedure is a novel translation of an entailment of symbolic heaps into a formula in Presburger arithmetic, and to combine it with an external SMT solver. This paper also gives experimental results by an implementation, which shows that the decision procedure works efficiently enough to use.

Daisuke Kimura, Makoto Tatsuta

Bringing Order to the Separation Logic Jungle

Abstract

Research results from so-called “classical” separation logics are not easily ported to so-called “intuitionistic” separation logics, and vice versa. Basic questions like, “Can the frame rule be proved independently of whether the programming language is garbage-collected?” “Can amortized resource analysis be ported from one separation logic to another?” should be straightforward. But they are not. Proofs done in a particular separation logic are difficult to generalize. We argue that this limitation is caused by incompatible semantics. For example, emp sometimes holds everywhere and sometimes only on units.

In this paper, we introduce a unifying semantics and build a framework that allows to reason parametrically over all separation logics. Many separation algebras in the literature are accompanied, explicitly or implicitly, by a preorder. Our key insight is to axiomatize the interaction between the join relation and the preorder. We prove every separation logic to be sound and complete with respect to this unifying semantics. Further, our framework enables us to generalize the sound0.ness proofs for the frame rule and CSL. It also reveals a new world of meaningful intermediate separation logics between “intuitionistic” and “classical”.

Qinxiang Cao, Santiago Cuellar, Andrew W. Appel

Concurrency and Verification

Frontmatter

Programming and Proving with Classical Types

Abstract

The propositions-as-types correspondence is ordinarily presented as linking the metatheory of typed \(\lambda \)-calculi and the proof theory of intuitionistic logic. Griffin observed that this correspondence could be extended to classical logic through the use of control operators. This observation set off a flurry of further research, leading to the development of Parigot’s \(\lambda \mu \)-calculus. In this work, we use the \(\lambda \mu \)-calculus as the foundation for a system of proof terms for classical first-order logic. In particular, we define an extended call-by-value \(\lambda \mu \)-calculus with a type system in correspondence with full classical logic. We extend the language with polymorphic types, add a host of data types in ‘direct style’, and prove several metatheoretical properties. All of our proofs and definitions are mechanised in Isabelle/HOL, and we automatically obtain an interpreter for a system of proof terms cum programming language—called \(\mu \)ML—using Isabelle’s code generation mechanism. Atop our proof terms, we build a prototype LCF-style interactive theorem prover—called \(\mu \)TP—for classical first-order logic, capable of synthesising \(\mu \)ML programs from completed tactic-driven proofs. We present example closed \(\mu \)ML programs with classical tautologies for types, including some inexpressible as closed programs in the original \(\lambda \mu \)-calculus, and some example tactic-driven \(\mu \)TP proofs of classical tautologies.

Cristina Matache, Victor B. F. Gomes, Dominic P. Mulligan

Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous

Abstract

We present in this paper a generic framework for the analysis of multi-threaded programs with recursive procedure calls, synchronisation by rendez-vous between parallel threads, and dynamic creation of new threads. To this end, we consider a model called Synchronized Dynamic Pushdown Networks (SDPNs) that can be seen as a network of pushdown processes executing synchronized transitions, spawning new pushdown processes, and performing internal pushdown actions. The reachability problem for this model is unfortunately undecidable. Therefore, we tackle this problem by introducing an abstraction framework based on Kleene algebras in order to compute an abstraction of the execution paths between two regular sets of configurations. We combine an automata theoretic saturation procedure with constraint solving in a finite domain. We then apply this framework to a Counter-Example Guided Abstraction Refinement (CEGAR) scheme, using multiple abstractions of increasing complexity and precision.

Adrien Pommellet, Tayssir Touili

Verified Root-Balanced Trees

Abstract

Andersson introduced general balanced trees, search trees based on the design principle of partial rebuilding: perform update operations naively until the tree becomes too unbalanced, at which point a whole subtree is rebalanced. We define and analyze a functional version of general balanced trees which we call root-balanced trees. Using a lightweight model of execution time, amortized logarithmic complexity is verified in the theorem prover Isabelle. Experimental results show competitiveness of root-balanced with AVL and red-black trees.

Tobias Nipkow

Safety and Liveness of MCS Lock—Layer by Layer

Abstract

The MCS Lock, a small but complex piece of low-level software, is a standard algorithm for providing inter-CPU locks with FIFO ordering guarantee and scalability. It is an interesting target for verification—short and subtle, involving both liveness and safety properties. We implemented and verified the MCS Lock algorithm as part of the CertiKOS kernel [8], showing that the C/assembly implementation contextually refines atomic specifications of the acquire and release lock methods. Our development follows the methodology of certified concurrent abstraction layers [7, 9]. By splitting the proof into layers, we can modularize it into separate parts for the low-level machine model, data abstraction, and reasoning about concurrent interleavings. This separation of concerns makes the layered methodology suitable for verified programming in the large, and our MCS Lock can be composed with other shared objects in CertiKOS kernel.

Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, Zhong Shao

Domain-Specific Languages

Frontmatter

Palgol: A High-Level DSL for Vertex-Centric Graph Processing with Remote Data Access

Abstract

Pregel is a popular distributed computing model for dealing with large-scale graphs. However, it can be tricky to implement graph algorithms correctly and efficiently in Pregel’s vertex-centric model, especially when the algorithm has multiple computation stages, complicated data dependencies, or even communication over dynamic internal data structures. Some domain-specific languages (DSLs) have been proposed to provide more intuitive ways to implement graph algorithms, but due to the lack of support for remote access — reading or writing attributes of other vertices through references — they cannot handle the above mentioned dynamic communication, causing a class of Pregel algorithms with fast convergence impossible to implement.

To address this problem, we design and implement Palgol, a more declarative and powerful DSL which supports remote access. In particular, programmers can use a more declarative syntax called chain access to naturally specify dynamic communication as if directly reading data on arbitrary remote vertices. By analyzing the logic patterns of chain access, we provide a novel algorithm for compiling Palgol programs to efficient Pregel code. We demonstrate the power of Palgol by using it to implement several practical Pregel algorithms, and the evaluation result shows that the efficiency of Palgol is comparable with that of hand-written code.

Yongzhe Zhang, Hsiang-Shang Ko, Zhenjiang Hu

Efficient Functional Reactive Programming Through Incremental Behaviors

Abstract

Many types of software are inherently event-driven ranging from web applications to embedded devices and traditionally, such applications are implemented using imperative callbacks. An alternative approach to writing such programs is functional reactive programming (FRP). FRP offers abstractions to make event-driven programming convenient, safe and composable, but they come at a price. FRP behaviors cannot efficiently deal with larger, incrementally constructed values such as a collection of messages or a list of connected devices. Since these situations occur naturally, it hinders the use of FRP. We report on a new FRP primitive: ‘incremental behavior’. We show that the semantics fit within existing FRP semantics and that their API can be used as a foundation for more ad-hoc solutions, such as incremental collections and discrete behaviors. Finally, we present benchmarks that demonstrate the advantages of incremental behaviors in terms of reduced computation time and bandwidth.

Bob Reynders, Dominique Devriese

Implementing Algebraic Effects in C

“Monads for Free in C”

Abstract

We describe an implementation of algebraic effects and handlers as a library in standard and portable C99, where effect operations can be used just like regular C functions. We use a formal operational semantics to guide the C implementation at every step where an evaluation context corresponds directly to a particular C execution context. Finally we show a novel extension to the semantics for optimized tail resumptions and prove it sound. This gives two orders of magnitude improvement to the performance of tail resumptive operations (up to about 150 million operations per second on a Core i7@2.6GHz).

Daan Leijen

Sound and Efficient Language-Integrated Query

Maintaining the ORDER

Abstract

As SQL moved from the English-like language for ad hoc queries by business users to its present status as the universal relational database access, the lack of abstractions and compositionality in the original design is felt more and more acute. Recently added subqueries and common table expressions compensate, albeit generally inefficiently. The inadequacies of SQL motivated language-integrated query systems such as (T-)LINQ, which offer an applicative, programming-like query language compiled to efficient SQL.

However, the seemingly straightforward ranking operations ORDER BY and LIMIT are not supported efficiently, consistently or at all in subqueries. The SQL standard defines their behavior only when applied to the whole query. Language-integrated query systems do not support them either: naively extending ranking to subexpressions breaks the distributivity laws of UNION ALL underlying optimizations and compilation.

We present the first compositional semantics of ORDER BY and LIMIT, which reproduces in the limit the standard-prescribed SQL behavior but also applies to arbitrarily composed query expressions and preserves the distributivity laws. We introduce the relational calculus SQUR that includes ordering and subranging and whose normal forms correspond to efficient, portable, subquery-free SQL. Treating these operations as effects, we describe a type-and-effect system for SQUR and prove its soundness. Our denotational semantics leads to the provably correctness-preserving normalization-by-evaluation. An implementation of SQUR thus becomes a sound and efficient language-integrated query system maintaining the ORDER.

Oleg Kiselyov, Tatsuya Katsushima

Semantics

Frontmatter

A Computational Interpretation of Context-Free Expressions

Abstract

We phrase parsing with context-free expressions as a type inhabitation problem where values are parse trees and types are context-free expressions. We first show how containment among context-free and regular expressions can be reduced to a reachability problem by using a canonical representation of states. The proofs-as-programs principle yields a computational interpretation of the reachability problem in terms of a coercion that transforms the parse tree for a context-free expression into a parse tree for a regular expression. It also yields a partial coercion from regular parse trees to context-free ones. The partial coercion from the trivial language of all words to a context-free expression corresponds to a predictive parser for the expression.

Martin Sulzmann, Peter Thiemann

Partiality and Container Monads

Abstract

We investigate monads of partiality in Martin-Löf type theory, following Moggi’s general monad-based method for modelling effectful computations. These monads are often called lifting monads and appear in category theory with different but related definitions. In this paper, we unveil the relationship between containers and lifting monads. We show that the lifting monads usually employed in type theory can be specified in terms of containers. Moreover, we give a precise characterization of containers whose interpretations carry a lifting monad structure. We show that these conditions are tightly connected with Rosolini’s notion of dominance. We provide several examples, putting particular emphasis on Capretta’s delay monad and its quotiented variant, the non-termination monad.

Tarmo Uustalu, Niccolò Veltri

The Negligible and Yet Subtle Cost of Pattern Matching

Abstract

The model behind functional programming languages is the closed \(\lambda \) -calculus, that is, the fragment of the \(\lambda \)-calculus where evaluation is weak (i.e. out of abstractions) and terms are closed. It is well-known that the number of \(\beta \) (i.e. evaluation) steps is a reasonable cost model in this setting, for all natural evaluation strategies (call-by-name/value/need). In this paper we try to close the gap between the closed \(\lambda \)-calculus and actual languages, by considering an extension of the \(\lambda \)-calculus with pattern matching. It is straightforward to prove that \(\beta \) plus matching steps provide a reasonable cost model. What we do then is finer: we show that \(\beta \) steps only, without matching steps, provide a reasonable cost model also in this extended setting—morally, pattern matching comes for free, complexity-wise. The result is proven for all evaluation strategies (name/value/need), and, while the proof itself is simple, the problem is shown to be subtle. In particular we show that qualitatively equivalent definitions of call-by-need may behave very differently.

Beniamino Accattoli, Bruno Barras

A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls

Abstract

In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, \(\lambda _\rho \), follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, \(\lambda _\rho ^\circ \), takes advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach.

Alejandro Díaz-Caro

Numerical Reasoning

Frontmatter

Compact Difference Bound Matrices

Abstract

The Octagon domain, which tracks a restricted class of two-variable inequalities, is the abstract domain of choice for many applications because its domain operations are either quadratic or cubic in the number of program variables. Octagon constraints are classically represented using a Difference Bound Matrix (DBM), where the entries in the DBM store bounds c for inequalities of the form \(x_i - x_j \leqslant c\), \(x_i + x_j \leqslant c\) or \(-x_i - x_j \leqslant c\). The size of such a DBM is quadratic in the number of variables, giving a representation which can be excessively large for number systems such as rationals. This paper proposes a compact representation for DBMs, in which repeated numbers are factored out of the DBM. The paper explains how the entries of a DBM are distributed, and how this distribution can be exploited to save space and significantly speed-up long-running analyses. Moreover, unlike sparse representations, the domain operations retain their conceptually simplicity and ease of implementation whilst reducing memory usage.

Aziem Chawdhary, Andy King

Sharper and Simpler Nonlinear Interpolants for Program Verification

Abstract

Interpolation of jointly infeasible predicates plays important roles in various program verification techniques such as invariant synthesis and CEGAR. Intrigued by the recent result by Dai et al. that combines real algebraic geometry and SDP optimization in synthesis of polynomial interpolants, the current paper contributes its enhancement that yields sharper and simpler interpolants. The enhancement is made possible by: theoretical observations in real algebraic geometry; and our continued fraction-based algorithm that rounds off (potentially erroneous) numerical solutions of SDP solvers. Experiment results support our tool’s effectiandveness; we also demonstrate the benefit of sharp and simple interpolants in program verification examples.

Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido, Ichiro Hasuo

A Nonstandard Functional Programming Language

Abstract

Nonstandard programming languages are the languages that deal with hyperreal numbers—real numbers extended with infinitesimal (i.e., smaller than any positive real) numbers—whose theory is given by nonstandard analysis (NSA). Nonstandard imperative language \(\mathbf {While}^\mathbf {dt}\) and nonstandard stream-processing language \(\mathbf {SProc}^\mathbf {dt}\) have been proposed so far and applied to hybrid system modeling and verification. We introduce a nonstandard functional language \(\textsc {NSF}\). We extend a simply typed functional language with a constant \(\mathbf {dt}\) that denotes an infinitesimal number and define its denotational semantics. The major challenge consists in giving the semantics of functions of an arbitrarily high order. To this end, we introduce *-cpos, a nonstandard counterpart of the standard domains.

Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga, Atsushi Igarashi

Counterexample-Guided Bit-Precision Selection

Abstract

Static program verifiers based on satisfiability modulo theories (SMT) solvers often trade precision for scalability to be able to handle large programs. A popular trade-off is to model bitwise operations, which are expensive for SMT solving, using uninterpreted functions over integers. Such an over-approximation improves scalability, but can introduce undesirable false alarms in the presence of bitwise operations that are common in, for example, low-level systems software. In this paper, we present our approach to diagnose the spurious counterexamples caused by this trade-off, and leverage the learned information to lazily and gradually refine the precision of reasoning about bitwise operations in the whole program. Our main insight is to employ a simple and fast type analysis to transform both a counterexample and program into their more precise versions that block the diagnosed spurious counterexample. We implement our approach in the SMACK software verifier, and evaluate it on the benchmark suite from the International Competition on Software Verification (SV-COMP). The evaluation shows that we significantly reduce the number of false alarms while maintaining scalability.

Shaobo He, Zvonimir Rakamarić

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

Invited Contributions

Frontmatter

Programming by Examples: PL Meets ML

Synthesizing SystemC Code from Delay Hybrid CSP

Security

Frontmatter

Taming Message-Passing Communication in Compositional Reasoning About Confidentiality

Capabilities for Java: Secure Access to Resources

Enforcing Programming Guidelines with Region Types and Effects

Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications

Heap and Equivalence Reasoning

Frontmatter

Black-Box Equivalence Checking Across Compiler Optimizations

Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects

Decision Procedure for Entailment of Symbolic Heaps with Arrays

Bringing Order to the Separation Logic Jungle

Concurrency and Verification

Frontmatter

Programming and Proving with Classical Types

Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous

Verified Root-Balanced Trees

Safety and Liveness of MCS Lock—Layer by Layer

Domain-Specific Languages

Frontmatter

Palgol: A High-Level DSL for Vertex-Centric Graph Processing with Remote Data Access

Efficient Functional Reactive Programming Through Incremental Behaviors

Implementing Algebraic Effects in C

Sound and Efficient Language-Integrated Query

Semantics

Frontmatter

A Computational Interpretation of Context-Free Expressions

Partiality and Container Monads

The Negligible and Yet Subtle Cost of Pattern Matching

A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls

Numerical Reasoning

Frontmatter

Compact Difference Bound Matrices

Sharper and Simpler Nonlinear Interpolants for Program Verification

A Nonstandard Functional Programming Language

Counterexample-Guided Bit-Precision Selection

Backmatter

Premium Partner