AstréeS

AstréeA is a static analyzer that can prove the absence of run-time errors in embedded software. But, to prove the correctness of a software system, we need to prove more than the end-user software: there are many layers under it, from libraries to hardware. When we look at the operating system, we need to prove more than safety properties: we need an analyzer for security.

Like AstréeA is built on Astrée, we build AstréeS (Astrée for Security) as an extension of AstréeA. Like Astrée and AstréeA, AstréeS is sound, automatic and aims to be scale up to real size programs. The theoretical background is also the same: AstréeS is based on abstract interpretation.

AstréeS started in the context of AnaStaSec ANR project.

To be able to analyze low-level software, like operating systems, AstréeS was extended in many ways. Most notable new feature is the analysis of mixed C and x86 assembly code. Another important feature is the addition of a new domain collaboration framework that allows abstract domains to share ghost variables managed in a very distributed way. It may be used to easily prove any properties that can be expressed with ghost variables.