The Trusted Platform Module (TPM) is a cryptoprocessor designed to protect integrity and security of modern computers. Communications with the TPM go through the TPM Software Stack (TSS). The open-source library tpm2-tss is a popular implementation of the TSS. Vulnerabilities in its code could allow attackers to recover sensitive information and take control of the system. This article presents a case study on formal verification of tpm2-tss using the Frama-C verification platform. Heavily based on linked lists and complex data structures, the library code appears to be highly challenging for the verification tool. We present several difficulties and tool limitations we faced, illustrate them with examples and describe solutions that allowed us to verify functional properties and the absence of runtime errors for a representative subset of functions. In particular, their verification required several lemmas proved in the interactive proof assistant Coq . We describe our verification results and desired tool improvements necessary to achieve a full formal verification of the target code.

Abstract Deductive verification tools can prove a large range of program properties, but often face issues on recursive data structures. Abstract interpretation tools based on separation logic and shape analysis can efficiently reason about such structures but cannot deal with so large classes of properties. This short paper presents an ongoing work on combining both techniques. We show how a deductive verifier for C programs, Frama-C/Wp, can benefit from a shape analysis tool, MemCAD, where structural and separation properties proved in the latter become assumptions for the former. A case study on selected functions of the tpm2-tss library using linked lists confirms the interest of the approach.

Testing and formal proving are two core methods for ensuring high software quality, with testing being a dynamic and proving a static analysis technique.The TAP (Tests and Proofs) conference series promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability.This special issue contains selected papers of the 14th and 15th edition of TAP in 2020 and 2021, respectively.Out of the 16 papers accepted for TAP 2020 and 2021, published by Springer in their LNCS series, 7 papers were invited for this special issue and 3 finally were accepted.The papers cover combinations of fuzzing, runtime assertion checking, automata learning (specifically an evaluation of different learning and testing algorithms), and program transformation:-"JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-Guided Fuzzing and Runtime Assertion Checking" by Amirfarhad Nilizadeh, Gary T. Leavens, Corina S. Pǎsǎreanu, and Yannic Noller, -"Benchmarking Combinations of Learning and Testing Algorithms for Automata Learning" by Bernhard K. Aichernig, Martin Tappler, and Felix Wallner, and -"Sound Runtime Assertion Checking for Memory Properties via Program Transformation" by Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, and Julien Signoles.

Runtime Assertion Checking (RAC) for expressive specification languages is a non-trivial verification task that becomes even more complex for memory-related properties of imperative languages with dynamic memory allocation. It is important to ensure the soundness of RAC verdicts, in particular when RAC reports the absence of failures for execution traces. This article presents a formalization of a program transformation technique for RAC of memory properties for a representative language with pointers and memory operations, including dynamic allocation and deallocation. The generated program instrumentation relies on an axiomatized observation memory model, which is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.

SyDPaCC (Systematic Development of programs for Parallel and Cloud Computing) is a framework for the Coq interactive theorem prover. It allows to systematically develop correct parallel programs from specifications via verified and automated program transformations. The obtained programs are scalable, i.e. able to run on numerous processors. SyDPaCC produces programs written in the multi-paradigm and functional programming language OCaml with calls to the BSML (Bulk Synchronous parallel ML) parallel programming library. In this paper we present ongoing work towards an extension of SyDPaCC to be able to produce Scala programs using Apache Spark for parallel processing.

International audience

Algorithmic skeletons are patterns of parallel computations. Skeletal parallel programming eases parallel programming: a program is merely a composition of such patterns. Data-parallel skeletons operate on parallel data-structures that have often sequential counterparts. In algorithmic skeleton approaches that offer a global view of programs, a parallel program has therefore a structure similar to a sequential program but operates on parallel data-structures. PySke is such an algorithmic skeleton library for Python to program shared or distributed memory parallel architectures in a simple way. This paper presents an extension to PySke: new algorithmic skeletons on parallel lists. This extension is evaluated on an application.

Skeletal parallelism offers a good trade-off between programming productivity and execution efficiency. In this style of parallelism, an application is a composition of algorithmic skeletons. An algorithmic skeleton captures a pattern of parallel algorithm on a distributed data structure, and is also often associated with a sequential algorithm on a sequential data structure that is the counterpart of the parallel data structure. The algorithmic skeleton approach has been inspired by functional programming. It is therefore very natural to embed algorithmic skeletons in a functional programming language. In this paper we present a new algorithmic skeleton library for the statically typed functional language OCaml, and illustrate its use on some applications. This functional skeletal parallel programming library is implemented using the Bulk Synchronous Parallel ML parallel programming library for OCaml.

Parallel programs based on the Divide&Conquer paradigm could be successfully defined in a simple way using powerlists. These parallel recursive data structures and their algebraic theories offer both a methodology to design parallel algorithms and parallel programming abstractions to ease the development of parallel applications. The paper presents how programs based on powerlists can be implemented in Java using the JPLF framework we developed. The design of this framework is based on powerlists theory, but in the same time follows the object-oriented design principles that provide flexibility and maintainability. Examples are given and performance experiments are conducted. The results emphasize the utility and the efficiency of the framework.

Frama-C is an extensible modular framework for analysis of C programs that offers different analyzers in the form of collaborating plugins. Currently, Frama-C does not support the proof of functional properties of concurrent code. We present Conc2Seq, a new code transformation based tool realized as a Frama-C plugin and dedicated to the verification of concurrent C programs. Assuming the program under verification respects an interleaving semantics, Conc2Seq transforms the original concurrent C program into a sequential one in which concurrency is simulated by interleavings. User specifications are automatically reintegrated into the new code without manual intervention. The goal of the proposed code transformation technique is to allow the user to reason about a concurrent program through the interleaving semantics using existing Frama-C analyzers.

It is difficult for customers to select the adequate cloud providers which fit their needs, as the number of cloud offerings increases rapidly. Many works thus focus on the design of cloud brokers. Unfortunately, most of them do not consider precise security requirements of customers. In this paper, we propose a methodology defined to place services in a multi-provider cloud environment, based on functional and non-functional requirements, including security requirements. To eliminate inner conflicts within customers requirements, and to match the cloud providers offers with these customers requirements, we use a formal analysis tool: Alloy. The broker uses a matching algorithm to place the required services in the adequate cloud providers, in a way that fulfills all customer requirements. We finally present a prototype implementation of the proposed broker.

We consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our contribution is a formal operational semantics of this language that satisfies a specification on execution traces designed in a companion paper.

With the current generalisation of parallel architectures arises the concern of applying formal methods to parallelism. The complexity of parallel, compared to sequential, programs makes them more error-prone and difficult to verify. Bulk Synchronous Parallelism (BSP) is a model of computation which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism. We propose a framework for refining a sequential specification toward a functional BSP program, the whole process being done with the help of the Coq proof assistant. To do so we define BH, a new homomorphic skeleton, which captures the essence of BSP computation in an algorithmic level, and also serves as a bridge in mapping from high level specification to low level BSP parallel programs.

Bulk Synchronous Parallel ML is a high-level language for programming parallel algorithms. Built upon OCaml and using the BSP model, it provides a safe setting for their implementation, avoiding concurrency related problems (deadlocks, indeterminism). Only a limited set of the features of OCaml can be used in BSML to respect its properties of safety: this paper describes a way to add exception handling to this set by extending and adapting OCaml 's exceptions. After a precise definition of the problems that arise and an informal description of the solutions, an extension of BSML is proposed. Formal semantics define the behaviour in all possible cases, followed by a short description of the implementation.

Bulk synchronous parallel ML (BSML) is an extension of the functional language Objective Caml to program bulk synchronous parallel (BSP) algorithms. It is deterministic, deadlock free and performances are good and predictable. Parallelism is expressed with a set of 4 primitives on a parallel data structure called parallel vector. These primitives are pure functional ones: they have no side-effect. It is thus possible, and we did it, to prove the correctness of BSML programs using a proof assistant like Coq. The BSlambda-calculus is an extension of the lambda-calculus which models the core semantics of BSML. Nevertheless some principles of BSML are not well captured by this calculus. This paper presents a new calculus, with a projection primitive, which provides a better model of the core semantics of BSML

Bulk synchronous parallel ML is a functional parallel language based on the bulk synchronous parallelism model of computation. Deadlocks are avoided and programs are deterministic. The performance of programs can be accurately predicted. This paper addresses the optimization of BSML programs through the compilation of BSML primitives to Objective Caml code with calls to a low level library rather than their direct implementation as a high level library.

This book describes theoretical results about AnsProlog * that have been obtained over the past decade.AnsProlog * or Prolog with Answer Sets 1 is a variation of the Prolog programming language, and extends the language by allowing clauses of the form:in the program.The L i 's are the literals (or atoms) of the Prolog language and may be supplied with a prefix ¬ sign, indicating the negation of a literal, while the prefix of not indicates negation as failure.Hence the semantics of the clause (C) may be read as follows: if all the literals L1, . . ., L m are true and all the literals L m+1 , . . ., L n can be safely assumed false then at least one of the literals L 1 , . . ., L k is true.(The actual semantics of each AnsProlog * program will be defined in terms of the Herbrand Universe of ground terms and the Herbrand Base of ground atoms.)The book takes the approach that the clause (C) is the most general form of a clause in the AnsProlog * language and so various subclasses of AnsProlog * can be defined by restricting this clause.For example: an AnsProlog -not program is when none of the clauses of a program contain the prefix not.In this respect, the book discusses the tractability, the complexity, the expressibility of the various subclasses of AnsProlog * based on the premise that AnsProlog * is both an excellent knowledge representation language and that it has a number of advantages over the Prolog language implementations based on SLDNF.For example, the ordering of goals within a clause and the ordering of clauses within a Prolog program affects whether a solution can or cannot be found (i.e. the program might get into an infinite loop); but not this is not the case within an AnsProlog * program.The reason being is that the semantics of an implementation of the AnsProlog * language can be thought of as allowing all models of the program to exist and then by using the clauses within the program, to impose restrictions on these models.The actual model(s) produced can then be interpreted in either a bi-valent (where a ground atom is either true or false) fashion or a tri-valent (where a ground atom is either true, false or unknown) fashion.The implementation algorithms describing how to restrict the models are described in Chapter 7 and two systems implementing the AnsProlog * language (and various subclasses), viz: (i) lparse+smodels and (ii) dlv are discussed in Chapter 8.The lparse+smodels program produces the stable models (or bi-valent) implementation, while the dlv produces the well-founded models (or tri-valent) implementation.Baral does note that both systems are under development and so implying that Chapter 8 may be out of date within a few years.However this aspect is compensated by Baral having a website www.baral.us/bookonewhere hypertext links to both the two systems and an errata/additional notes for the book are presented.On the application side, the book is peppered with many examples and simple programs illustrating the current point being made in the text.For example: how various forms of the 1 AnsProlog * is sometimes called A-Prolog in the literature.