Selected Papers of the 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2019)

Editors: Jorge A. Pérez and Nobuko Yoshida

1. Psi-Calculi Revisited: Connectivity and Compositionality

Johannes Åman Pohjola.
Psi-calculi is a parametric framework for process calculi similar to popularpi-calculus extensions such as the explicit fusion calculus, the appliedpi-calculus and the spi calculus. Mechanised proofs of standard algebraic andcongruence properties of bisimilarity apply to all calculi within theframework. A limitation of psi-calculi is that communication channels must besymmetric and transitive. In this paper, we give a new operational semantics topsi-calculi that allows us to lift these restrictions and simplify some of theproofs. The key technical innovation is to annotate transitions with aprovenance -- a description of the scope and channel they originate from. Wegive mechanised proofs that our extension is conservative, and that thestandard algebraic and congruence properties of strong and weak bisimilarityare maintained. We show correspondence with a reduction semantics and barbedbisimulation. We show how a pi-calculus with preorders that was previouslybeyond the scope of psi-calculi can be captured, and how to encode mixed choiceunder very strong quality criteria.

2. Correct and Efficient Antichain Algorithms for Refinement Checking

Maurice Laveaux ; Jan Friso Groote ; Tim A. C. Willemse.
The notion of refinement plays an important role in software engineering. Itis the basis of a stepwise development methodology in which the correctness ofa system can be established by proving, or computing, that a system refines itsspecification. Wang et al. describe algorithms based on antichains forefficiently deciding trace refinement, stable failures refinement andfailures-divergences refinement. We identify several issues pertaining to thesoundness and performance in these algorithms and propose new, correct,antichain-based algorithms. Using a number of experiments we show that ouralgorithms outperform the original ones in terms of running time and memoryusage. Furthermore, we show that additional run time improvements can beobtained by applying divergence-preserving branching bisimulation minimisation.

3. Output-sensitive Information flow analysis

Cristian Ene ; Laurent Mounier ; Marie-Laure Potet.
Constant-time programming is a countermeasure to prevent cache based attackswhere programs should not perform memory accesses that depend on secrets. Insome cases this policy can be safely relaxed if one can prove that the programdoes not leak more information than the public outputs of the computation. Wepropose a novel approach for verifying constant-time programming based on a newinformation flow property, called output-sensitive noninterference.Noninterference states that a public observer cannot learn anything about theprivate data. Since real systems need to intentionally declassify someinformation, this property is too strong in practice. In order to take intoaccount public outputs we proceed as follows: instead of using complex explicitdeclassification policies, we partition variables in three sets: input, outputand leakage variables. Then, we propose a typing system to statically checkthat leakage variables do not leak more information about the secret inputsthan the public normal output. The novelty of our approach is that we track thedependence of leakage variables with respect not only to the initial values ofinput variables (as in classical approaches for noninterference), but takingalso into account the final values of output variables. We adapted thisapproach to LLVM IR and we developed a prototype to verify LLVMimplementations.

4. Parametric updates in parametric timed automata

Étienne André ; Didier Lime ; Mathias Ramparison.
We introduce a new class of Parametric Timed Automata (PTAs) where we allowclocks to be compared to parameters in guards, as in classic PTAs, but also tobe updated to parameters. We focus here on the EF-emptiness problem: "is theset of parameter valuations for which some given location is reachable in theinstantiated timed automaton empty?". This problem is well-known to beundecidable for PTAs, and so it is for our extension. Nonetheless, if we updateall clocks each time we compare a clock with a parameter and each time weupdate a clock to a parameter, we obtain a syntactic subclass for which we candecide the EF-emptiness problem and even perform the exact synthesis of the setof rational valuations such that a given location is reachable. To the best ofour knowledge, this is the first non-trivial subclass of PTAs, actually evenextended with parametric updates, for which this is possible.