Showing 1–7 of 7 results for author: Mounier, L

Function synthesis for maximizing model counting

Authors: Thomas Vigouroux, Marius Bozga, Cristian Ene, Laurent Mounier

Abstract: Given a boolean formula $Φ$(X, Y, Z), the Max\#SAT problem asks for finding a partial model on the set of variables X, maximizing its number of projected models over the set of variables Y. We investigate a strict generalization of Max\#SAT allowing dependencies for variables in X, effectively turning it into a synthesis problem. We show that this new problem, called DQMax\#SAT, subsumes both the… ▽ More Given a boolean formula $Φ$(X, Y, Z), the Max\#SAT problem asks for finding a partial model on the set of variables X, maximizing its number of projected models over the set of variables Y. We investigate a strict generalization of Max\#SAT allowing dependencies for variables in X, effectively turning it into a synthesis problem. We show that this new problem, called DQMax\#SAT, subsumes both the DQBF and DSSAT problems. We provide a general resolution method, based on a reduction to Max\#SAT, together with two improvements for dealing with its inherent complexity. We further discuss a concrete application of DQMax\#SAT for symbolic synthesis of adaptive attackers in the field of program security. Finally, we report preliminary results obtained on the resolution of benchmark problems using a prototype DQMax\#SAT solver implementation. △ Less

Submitted 12 September, 2023; v1 submitted 17 May, 2023; originally announced May 2023.

A tool assisted methodology to harden programs against multi-faults injections

Authors: Etienne Boespflug, Abderrahmane Bouguern, Laurent Mounier, Marie-Laure Potet

Abstract: Fault attacks consist in changing the program behavior by injecting faults at run-time in order to break some expected security properties. Applications are hardened against fault attack adding countermeasures. According to the state of the art, applications must now be protected against multi-fault injection. As a consequence develo** applications which are robust becomes a very challenging tas… ▽ More Fault attacks consist in changing the program behavior by injecting faults at run-time in order to break some expected security properties. Applications are hardened against fault attack adding countermeasures. According to the state of the art, applications must now be protected against multi-fault injection. As a consequence develo** applications which are robust becomes a very challenging task, in particular because countermeasures can be also the target of attacks. The aim of this paper is to propose an assisted methodology for developers allowing to harden an application against multi-fault attacks, addressing several aspects: how to identify which parts of the code should be protected and how to choose the most appropriate countermeasures, making the application more robust and avoiding useless runtime checks. △ Less

Submitted 3 March, 2023; originally announced March 2023.

BAXMC: a CEGAR approach to Max#SAT

Authors: Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet

Abstract: Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free propositional formula compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix. We propose a CEGAR-based algorithm and refinements thereof… ▽ More Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free propositional formula compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix. We propose a CEGAR-based algorithm and refinements thereof, based on either exact or approximate model counting, and prove its correctness in both cases. Our experiments show that this algorithm has much better effective complexity than the state of the art. △ Less

Submitted 6 February, 2023; v1 submitted 2 November, 2022; originally announced November 2022.

Comments: FMCAD 2022, Oct 2022, Trente, Italy

Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine

Authors: Frédéric Recoules, Sébastien Bardin, Richard Bonichon, Matthieu Lemerre, Laurent Mounier, Marie-Laure Potet

Abstract: Inline assembly is still a common practice in low-level C programming, typically for efficiency reasons or for accessing specific hardware resources. Such embedded assembly codes in the GNU syntax (supported by major compilers such as GCC, Clang and ICC) have an interface specifying how the assembly codes interact with the C environment. For simplicity reasons, the compiler treats GNU inline assem… ▽ More Inline assembly is still a common practice in low-level C programming, typically for efficiency reasons or for accessing specific hardware resources. Such embedded assembly codes in the GNU syntax (supported by major compilers such as GCC, Clang and ICC) have an interface specifying how the assembly codes interact with the C environment. For simplicity reasons, the compiler treats GNU inline assembly codes as blackboxes and relies only on their interface to correctly glue them into the compiled C code. Therefore, the adequacy between the assembly chunk and its interface (named compliance) is of primary importance, as such compliance issues can lead to subtle and hard-to-find bugs. We propose RUSTInA, the first automated technique for formally checking inline assembly compliance, with the extra ability to propose (proven) patches and (optimization) refinements in certain cases. RUSTInA is based on an original formalization of the inline assembly compliance problem together with novel dedicated algorithms. Our prototype has been evaluated on 202 Debian packages with inline assembly (2656 chunks), finding 2183 issues in 85 packages -- 986 significant issues in 54 packages (including major projects such as ffmpeg or ALSA), and proposing patches for 92% of them. Currently, 38 patches have already been accepted (solving 156 significant issues), with positive feedback from development teams. △ Less

Submitted 15 February, 2021; originally announced February 2021.

Output-sensitive Information flow analysis

Authors: Cristian Ene, Laurent Mounier, Marie-Laure Potet

Abstract: Constant-time programming is a countermeasure to prevent cache based attacks where programs should not perform memory accesses that depend on secrets. In some cases this policy can be safely relaxed if one can prove that the program does not leak more information than the public outputs of the computation. We propose a novel approach for verifying constant-time programming based on a new informati… ▽ More Constant-time programming is a countermeasure to prevent cache based attacks where programs should not perform memory accesses that depend on secrets. In some cases this policy can be safely relaxed if one can prove that the program does not leak more information than the public outputs of the computation. We propose a novel approach for verifying constant-time programming based on a new information flow property, called output-sensitive noninterference. Noninterference states that a public observer cannot learn anything about the private data. Since real systems need to intentionally declassify some information, this property is too strong in practice. In order to take into account public outputs we proceed as follows: instead of using complex explicit declassification policies, we partition variables in three sets: input, output and leakage variables. Then, we propose a ty** system to statically check that leakage variables do not leak more information about the secret inputs than the public normal output. The novelty of our approach is that we track the dependence of leakage variables with respect not only to the initial values of input variables (as in classical approaches for noninterference), but taking also into account the final values of output variables. We adapted this approach to LLVM IR and we developed a prototype to verify LLVM implementations. △ Less

Submitted 11 February, 2021; v1 submitted 20 September, 2019; originally announced September 2019.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 1 (February 12, 2021) lmcs:5779

Get rid of inline assembly through verification-oriented lifting

Authors: Frédéric Recoules, Sébastien Bardin, Richard Bonichon, Laurent Mounier, Marie-Laure Potet

Abstract: Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable forthcoming challenges. For example, C programmers regularly use inline assembly for low-level optimizations and system primitives. This usually resu… ▽ More Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable forthcoming challenges. For example, C programmers regularly use inline assembly for low-level optimizations and system primitives. This usually results in driving state-of-the-art formal analyzers developed for C ineffective. We thus propose TInA, an automated, generic, trustable and verification-oriented lifting technique turning inline assembly into semantically equivalent C code, in order to take advantage of existing C analyzers. Extensive experiments on real-world C code with inline assembly (including GMP and ffmpeg) show the feasibility and benefits of TInA. △ Less

Submitted 1 October, 2019; v1 submitted 15 March, 2019; originally announced March 2019.

Combining Static and Dynamic Analysis for Vulnerability Detection

Authors: Sanjay Rawat, Dumitru Ceara, Laurent Mounier, Marie-Laure Potet

Abstract: In this paper, we present a hybrid approach for buffer overflow detection in C code. The approach makes use of static and dynamic analysis of the application under investigation. The static part consists in calculating taint dependency sequences (TDS) between user controlled inputs and vulnerable statements. This process is akin to program slice of interest to calculate tainted data- and control-f… ▽ More In this paper, we present a hybrid approach for buffer overflow detection in C code. The approach makes use of static and dynamic analysis of the application under investigation. The static part consists in calculating taint dependency sequences (TDS) between user controlled inputs and vulnerable statements. This process is akin to program slice of interest to calculate tainted data- and control-flow path which exhibits the dependence between tainted program inputs and vulnerable statements in the code. The dynamic part consists of executing the program along TDSs to trigger the vulnerability by generating suitable inputs. We use genetic algorithm to generate inputs. We propose a fitness function that approximates the program behavior (control flow) based on the frequencies of the statements along TDSs. This runtime aspect makes the approach faster and accurate. We provide experimental results on the Verisec benchmark to validate our approach. △ Less

Submitted 16 May, 2013; originally announced May 2013.

Comments: There are 15 pages with 1 figure