research
∙
02/23/2023
ProSpeCT: Provably Secure Speculation for the Constant-Time Policy (Extended version)
We propose ProSpeCT, a generic formal processor model providing provably...
share
research
∙
12/10/2022
A Quantitative Flavour of Robust Reachability
Many software analysis techniques attempt to determine whether bugs are ...
research
∙
10/24/2022
Scalable Program Clone Search Through Spectral Analysis
We consider the problem of program clone search, i.e. given a target pro...
research
∙
09/02/2022
Binsec/Rel: Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-Erasure
This paper tackles the problem of designing efficient binary-level verif...
research
∙
09/14/2021
Formal Methods for Quantum Programs: A Survey
While recent progress in quantum hardware open the door for significant ...
research
∙
02/15/2021
Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine
Inline assembly is still a common practice in low-level C programming, t...
research
∙
02/09/2021
AI-based Blackbox Code Deobfuscation: Understand, Improve and Mitigate
Code obfuscation aims at protecting Intellectual Property and other secr...
research
∙
11/30/2020
No Crash, No Exploit: Automated Verification of Embedded Kernels
The kernel is the most safety- and security-critical component of many c...
research
∙
03/19/2020
Automatically Proving Microkernels Free from Privilege Escalation from their Executable
Operating system kernels are the security keystone of most computer syst...
research
∙
03/12/2020
A Deductive Verification Framework for Circuit-building Quantum Programs
While recent progress in quantum hardware open the door for significant ...
research
∙
02/25/2020
Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities
Directed fuzzing focuses on automatically testing specific parts of the ...
research
∙
12/18/2019
Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level
The constant-time programming discipline (CT) is an efficient countermea...
research
∙
08/05/2019
How to Kill Symbolic Deobfuscation for Free; or Unleashing the Potential of Path-Oriented Protections
Code obfuscation is a major tool for protecting software intellectual pr...
research
∙
03/15/2019
Get rid of inline assembly through trustable verification-oriented lifting
Formal methods for software development have made great strides in the l...
research
∙
02/15/2018
Model Generation for Quantified Formulas: A Taint-Based Approach
We focus in this paper on generating models of quantified first-order fo...
research
∙
12/28/2017
Abstract Interpretation using a Language of Symbolic Approximation
The traditional abstract domain framework for imperative programs suffer...
research
∙
08/29/2017
Freeing Testers from Polluting Test Objectives
Testing is the primary approach for detecting software defects. A major ...
research
∙
12/01/2013