Date: November 20, 2018
Place: A008
Chairs: Emmanuel Jeandel
9h15-9h30 Welcome
Session 1 : 9h30-10h30
Joseph Lallemand
Voting: You Can’t Have Privacy without Individual Verifiability #T5
Electronic voting typically aims at two main security goals: vote privacy and verifiability. These two goals are often seen as antagonistic and some national agencies even impose a hierarchy between them: first privacy, and then verifiability as an additional feature. Verifiability typically includes individual verifiability (a voter can check that her ballot is counted); universal verifiability (anyone can check that the result corresponds to the published ballots); and eligibility verifiability (only legitimate voters may vote). We show that actually, privacy implies individual verifiability. In other words, systems without individual verifiability cannot achieve privacy (under the same trust assumptions). To demonstrate the generality of our result, we show this implication in two different settings, namely cryptographic and symbolic models, for standard notions of privacy and individual verifiability. Our findings also highlight limitations in existing privacy definitions in cryptographic settings.
Hans-Jorg Schurr
Towards really neat proofs for SMT #T9
veriT is a state of the art Satisfiability Modulo Theories (SMT) solver. Given an unsatisfiable input problem, veriT can output a certificate – a proof – of its unsatisifiability. These proofs serve at least two purposes. On the one hand, they can be checked by an external proof checker, relieving the SMT solver from the responsibility of being trustworthy, on the other hand they can be used by client systems for further processing. In the past the proofs generated by veriT have been partially reconstructed in the interactive theorem prover Isabelle/HOL. We discuss ongoing work on improving SMT proof production. While work is constrained by the architecture of the SMT solver, the requirements on the format are given by typical use cases. Overall, our goal is to ensure veriT produces proofs which are easy to check, while maintaining performance.
10h30-11h00 : Coffee
Session 2 : 11h00-12h30
Nicolas Schnepf
Orchestration and verification of security functions for smart environments #T8
Security threats against smart environments are exponentially growing for several years due to lack of market preventive methods. A solution proposed by researchers consists in chaining security functions for dynamically protecting those devices: in particular, those chains would benefit of the programmability provided by software defined networks (SDN) for automating their deployment and their adjustment. Nevertheless, the multiplication and the complexity of such chains of security functions increase the risk of introducing misconfigurations in network policies: because of this complexity, the validation of such chains require the use of formal methods for guarantying their correctness before their deployment.
The goal of this PhD is to design a framework for the orchestration and the verification of chains of security functions. In our previous work we already designed an approach for the validation of security policy called synaptic: this framework relies on formal methods for validating the correctness of SDN policies. Complementary to this work we proposed an approach for automatically profiling android applications in order to identify their security requirements. The remaining part of our work will consist in designing an approach for automatically generating or selecting chains of security functions corresponding to the applications running on a device.
Sylvain Cecchetto
BOA : a CFG builder (by Basic blOck Analysis) based on system state prediction #T1
This research is targeting people who want to study a binary for which the do not have the source code. These people include malware analysts who want to be able to understand the behavior and or the dangerousness of an unknown program. We can also think about reversers who might want to be able to extract and recover the code of a specific part of a binary, or, also to analyse a program used in a constrained environment like an airplane, in order to evaluate the risks that it crash or reach an unwanted state. Overall, this research can be useful in domains like malware detection, reverse engineering and system protections. In order to analyse the behavior of a program for which we do not have the source code (typically in a malware analysis case), it is almost mandatory for the analyst to disassemble its binary code, that is to list all program instructions. However, as Schwarz, Debray ans Andrews explained, the disassembly step is undecidable due to dynamic jumps instructions. Unfortunately, the problem remains, and partial solutions are based on heuristics. Two properties are desired during this step, (i) the completeness that aims to recover all instructions that the binary contains without missing and (ii) the correction that aims to only disassemble instructions that can be executed. Furthermore, we have to deal with obfuscated binaries. obfuscation techniques are designed to protect code/program against human and automated analysis. The obfuscation can be legitimate to protect intellectual property or doubtful in the case of a malware because the author want to slow down the analyst. In 2003, Linn and Debray expose some obfuscated techniques in order to make loose any standard disassembly tool. On another side, Kruegel, Robertson, Valeur and Vigna in 2004 propose to add some improvement on existing disassembly algorithms in order to be able to disassemble obfuscated binaries like the ones build with the Linn and Debray techniques. Finally we are facing the game of cat and mouse between, in the first side, always better obfuscated techniques and in other side, disassembly tools that have to be more and more robust. Usually, the disassembly step is followed by the control flow graph reconstruction. This step aims to construct an oriented graph from the basic blocks (previously obtained during disassembly) in which the links describe the different paths that the binary can take during an execution. This construction is undecidable in general since it involves variable values during execution. Furthermore, as we said, obfuscation techniques like self-code-modification, call stack tampering or opaque predicate can make difficult both, disassembly and control flow graph constructions steps.
In order to improve the disassembly and control flow graph constructions steps some works have be done based on symbolic execution techniques like it is shown by Yadegari and Debray in 2015. As Schwartz, Avgerinos and Brumley said in 2010, this method allows to reason about the behavior of a program on many different inputs at one time by building a logical formula that represents a program execution. In this paper we propose a new approach called BOA (for Basic blOck Analysis) to solve (at least partially) the disassembly and control flow graph construction problems. This method is based on symbolic execution at a basic block level. This technique aims to compute a partial system state as pre and post conditions of BB. Then, from this partial system state we can compute dynamic jump/call instructions target addresses, detect call stack tampering, opaque predicate or self-code-modifications.
Pierre Lermusiaux
Analysing algebraic type transformations with Pass Rewriting #T6
Program transformation is a common practice in computer science, and its many applications can have a range of different objectives. For example, a program written in an original high level language could be either translated into machine code for execution purposes, or towards a language suitable for formal verification. In all cases, the transformation is often realized in several phases, called passes, each performing a smaller transformation, thus going through a number of intermediate languages. While languages often have a lot of different constructions, only a few are generally concerned for each one of these passes. Some languages, such as Tom and Stratego, use rewriting strategies to effectively implement traversal operation so as to not have to deal with unchanged constructions. Another interesting solution, with a similar pattern matching approach, is proposed by the Nanopass framework: using autogeneration techniques on these same trivial cases. In order to ensure the correctness of the overall transformation, w.r.t. the target language, each pass should be able to guarantee that the intermediate program is well-formed in the context of its corresponding language. However, neither mentioned solution manages to satisfyingly provide such guarantees.
Therefore, we propose a new formalism for transformation techniques, based on pattern matching and rewriting, with an expressive power comparable to above solutions. Moreover, it will enable statically performing type analysis on the transformation, in order to improve on their limitation. The interest of this formalism will be largely based on this type analysis, which would allow the definition of transformations in a general context while still providing syntactical guarantees.
12h30-14h00 : Lunch
Session 3 : 14h-15h30
Charlie Jacomme
Symbolic methods applied to the automation of computational proofs #T4
After having introduced two classical models used in the formal verification of security protocols – the Symbolic model and the Computational model – we will show how the former may be used to improve proofs automation in the latter.
Renaud Vilmart
A Simplified ZX-Calculus for Universal Quantum Computing #T10
The ZX-Calculus is a powerful graphical language for reasoning about quantum processes and quantum computing. It has various applications, ranging from foundations of quantum mechanics and models of quantum computation, to compilation of quantum circuits, quantum error correction, … Complete axiomatisations have recently been provided for the first approximately universal fragment of the language, and right after that for the whole language. These axiomatisations, even though complete, suffered one major drawback: some of their axioms involve a lot of nodes, and consequently they are hard to use, and their interpretations are far-fetched, if not non-existent. We provide a simplified axiomatisation for the general ZX-Calculus, giving the calculus one of its main initial features back: intuitiveness.
Daniel El Ouraoui
Machine learning for instance selection in SMT solving #T3
Satisfiability modulo theories (SMT) solvers have increased their capabilities to solve many different problems with the development of ever more effective decision procedures. Hence state of the art SMT solvers have now established themselves as one of the best solutions to tackle ground quantifier-free first order problems. Nevertheless, automated theorem provers (ATP) based on superposition techniques remain incredibly better to handle quantified formulas. One reason is that they are fully understanding the semantics of quantifiers, whereas SMT solvers try to heuristically find a set of instances which could lead to solve the grounded problem. Often, these techniques produce a very large number of instances, many of them being useless. Generally, only 10% of the instances are useful. This often explains why SMT solvers fail to prove simple first order problems. We suggest to apply state of the art machine learning techniques as classifiers for instances on top of the process. We show that such techniques can indeed lead to significantly smaller numbers of generated instances, and even more, can be used to solve new problems that could not be solved before.
15h30-16h : Coffee
Session 4 : 16h-17h
Margaux Duroeulx
Satisfiability techniques for assessing systems reliability #T2
Fault trees (FTs) or reliability block diagrams are commonly used representations for the reliability assessment of systems. In our work, we aim at using satisfiability (SAT) techniques as a building block in this analysis, based on the computation of minimal cut sets or tie sets from the system’s structure function. We previously introduced the use of SAT techniques for computing tie sets of systems with a structure function that depends only on the working status of components. We now extend the approach to systems where the order of failures matters, and that can be represented by a dynamic fault tree (DFT).
Beyond the gates available in an ordinary FT (such as conjunction, disjunction or k out of n), a DFT may contain three types of dynamic gates indicating priority conjunction, functional dependency, and spare components. The corresponding structure function depends not only on the working status of components but also on the temporal order between component failures, represented by additional propositional variables in the SAT encoding. The appropriate generalization of a tie set is then a Tie Set with Sequence (TSS). Whereas an ordinary tie set only reflects the set of components that are functioning correctly, a TSS also records the order in which component failures occurred. Standard tie and cut sets can be organized in a Hasse diagram that reflects the complete partial order between these configurations due to component failures, and the Hasse diagram provides a convenient basis for computing the reliability function. We show that this representation extends to tie and cut set sequences.
Our approach generates the structure function from a DFT, uses a SAT solver for efficiently computing the minimal TSSs, and obtains the reliability polynomial based on the positions of the TSSs in the Hasse diagram. According to the type of analysis the user is interested in, our method can therefore provide qualitative results in the form of tie set sequences or quantitative results by computing the probability of system failure after a given period of time.
Itsaka Rakotonirina
Symmetries of equivalence in security protocols #T7
Security protocols are distributed programs specifying how some agents can exchange some messages remotely, through an untrusted network. These protocols are expected to offer some privacy guarantees against dishonnest parties controlling the communication network, but their analysis has proved tedious and error-prone when performed by hand. Efficient automated tools exist to support flaw detection, e.g. the recent DEEPSEC prover, but still have some shortcomings in terms of scalability (the underlying theoretical problem exhibiting a high complexity). In this work we present techniques exploiting the properties that typical systems have, e.g. internal symmetries, to reduce the practical cost of performing security analyses and therefore improve on the scope automated analysers. An implementation of these techniques is in progress.
