Toward Automated Vulnerability Analysis – TAVA

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 and 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 the AVABOX, 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).