Partners: CEA List (Saclay), AMOSSYS, Verimag/PACS
The Internet of Things opens a new era of global and powerful attacks carried out by compromised devices.Manual responses cannot deal with the increased danger that these threats represent. It is therefore necessary to use automatic methods for vulnerability detection, in particular to replay analysis for certification purposes. State-of-the-art techniques (fuzzing,symbolic execution) face 3 main challenges:complex vulnerability detection,criticality assessment of vulnerabilities (taking attacker capabilities into account) and scalability. TAVA combines the most salient aspects of formal methods, symbolic &static, and security for automatic and efficient detection and assessment of complex vulnerabilities. The project will yield three main outcomes:
- science: it will lay the foundation of a vulnerability-oriented program analysis framework– as opposed to current bug-oriented approaches, with new theory, algorithms and tools and taking into account dedicated attacker models and exploitability;
- technology: it will develop theAVABOX, an automated toolset for supporting IoT evaluation and certification incorporating unique capabilities in terms of vulnerability assessment and attacker modelization. Also, as the AVABOX builds on the BINSEC open-source platform, TAVA will provide the opportunity to strongly consolidate it, with the ambition to become a reference platform for formal binary-level program analysis;
- valorization AMOSSYS will take full advantage of the project to improve its line of products and services through the AVABOX toolset. Especially, it evaluates the interest of the approach on several case-studies representative of IoT security evaluation, and propose guidelines for a productive integration of the tool in the certification process (Common Criteria schemes, CSPN and the incoming European schemes)
