CE39 - Sécurité globale, résilience et gestion de crise, cybersécurité

EMASS: Effective Memory Analysis of Systems Software – EMASS

Submission summary

Memory corruption in systems software written in memory-unsafe language, like C or assembly, is still today the source of most severe and frequent security vulnerabilities. In addition to memory safety, many security properties apply to values flowing through the memory. The project will provide an effective way to verify memory-related security properties for systems programs, from source or from their compiled executable. We will focus in particular on memory safety and information flow properties, like separation between tasks in an OS kernel or between connections in an SSL library.

This method will rely on a static analysis using lightweight and simple type annotations, that we developped in a preliminary work to verify security properties like absence of privilege escalation in a small microkernel [RTAS 2021, best paper]. Inspired by this initial prototype, we want to address notoriously difficult challenges that must be overcome to be usable industrially and have a practical security impact, such as scaling the analysis to large code bases, being able to verify information-flow properties, or improving precision on challenging code patterns, all this while keeping the amount of manual effort low.

The project will be performed by a strong consortium gathering experts in the design of static analyzers; static analysis of C, machine code, or OS kernels; automated verification of cybersecurity properties; or applying formal methods in the industry.

The project outcome will result in efficient static analysis tools for verifying memory-related security properties on system code, together with an industrial methodology demonstrated on real use cases. It will propose new abstractions and tools that will impact scientific fields such as cybersecurity, formal methods, software engineering, and systems; and will also impact industrial users in need of securing their systems software.

Project coordination

Matthieu LEMERRE (COMMISSARIAT A L' ENERGIE ATOMIQUE ET AUX ENERGIES ALTERNATIVES)

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

Partner

TRT Thales Research Technology
CEA/LIST COMMISSARIAT A L' ENERGIE ATOMIQUE ET AUX ENERGIES ALTERNATIVES
Institut national de la recherche en informatique et automatique

Help of the ANR 679,390 euros
Beginning and duration of the scientific project: - 42 Months

Useful links

Explorez notre base de projets financés

 

 

ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter