AnaStaSec: challenges
|
Analysis for Security Properties.
Objectives
The main objective of this project is to show that formal methods are mature enough to be used for proving the security of large-scale software intensive industrial systems during the development and the production of these systems, and that these approaches can offer a less costly or more reliable alternative to the methods which are used usually (mainly methods based on process assurance and exploratory tests).
In particular, the security properties of software-intensive industrial case studies will be formally specified and then proved automatically, thanks to a set of prototype tools that will be designed during the project. We will focus on the analysis of some case studies provided by Airbus. More precisely, the secrecy and the authenticity of messages in cryptographic protocols envisioned to secure datalink communications will be addressed at model and implementation levels. Then, a large software-intensive system will be analysed. This system is composed of a trusted host platform (including a real-time operating system, communication protocols, routers, application monitoring), some trusted datalink applications implementing air traffic control functions, and some less trusted datalink applications -- the source of which is not available.
Scientific challenges
The main scientific locks are:
- the formalisation of the security properties for a software intensive industrial system;
- making formal methods in security scale to large industrial cases;
- the proof of the security properties of complex industrial communication protocols (both at model and implementation levels);
- the proof of the security of systems, in which security properties and complex software properties are closely entangled (for instance because security properties may depend on complex properties about data-structures or complex properties about the synchronisation of the distributed threads);
- the proof of security and isolation of subsystems where only the binary code of untrusted application is available.
Outcomes
We expect many important scientific outcomes. Firstly, this project will empirically prove that formal methods can be used to prove the security of large scale industrial complex software-intensive systems, which will validate a lot of research in this area. Then several techniques and tools will be designed or enhanced. For instance, the analysis of source code will provide new abstract domains to deal with security properties. These abstract domains will establish precise relational properties about trace prefixes and field values, which can be relevant in other application domains. Our project also involves more exploratory parts such as the use of event structure reduction techniques to reconstruct minimal attacks and the certification of a compiler ensuring the preservation of security properties. This works are likely to improve the state of the art in these fields.
There will be also many crucial industrial and economical outcomes. The project will enhance the state of the art of security evaluation processes in the secure IT and avionics industries. In the medium term, AnaStaSec formal methods and tools should become relevant also for other domains embedding networked critical systems, e.g. automotive or railway.
We will promote technologies towards developers of secure software and standard authorities. In particular, an effort will be made for the dissemination of the AnaStaSec static analysis results in the security evaluation community. Current practice relies mostly on process assurance, and sophisticated, exploratory testing. Relying solely on such approaches for security assurance would bring only limited trust, while increasing verification costs by about 40%. Considering verification already represents over 50% of the development costs of such systems, this would yield huge cost increases, typically several million euros for the development of a single avionics system, or the upgrade of a legacy system to deal with new security-related constraints. Taking into account the very large number of legacy systems developed with little security requirements that will most likely need security evaluations, and possibly important security-related upgrades in the next decade, the financial benefit of static analysis for security properties will be paramount.