Flaminia Luccio
Ca' Foscari University of Venice
| e‑mail: |
|
|---|
ALVIE is an automated tool for security analysis of embedded hardware architectures, bridging the gap between formal verification and vulnerability research. It was developed to evaluate Sancus, an embedded security architecture that remains susceptible to implementation bugs. ALVIE constructs formal models of hardware systems using black-box active automata learning and applies model checking to detect potential side-channels, enabling formal verification of security properties on real implementations.
Core Features
ALVIE combines active automata learning and model checking to automatically analyze hardware security without requiring detailed knowledge of the design internals. Users can configure the tool to focus on specific attackers or target classes, producing formal models and identifying side-channel vulnerabilities.
Key Benefits
ALVIE enables systematic, high-confidence assessment of embedded hardware security, complementing formal verification methods by uncovering implementation-level vulnerabilities. With the upcoming support for FPGA platforms and RISC-V, ALVIE promises to improve speed, efficiency, and applicability in industrial settings, providing a robust framework for hardware security evaluation and proactive mitigation of potential threats.
Areas of Application
ALVIE is intended for evaluating security architectures in embedded hardware, including Sancus-based designs, RISC-V and FPGA implementations. The tool’s adaptability allows its application to other secure hardware designs, supporting companies that develop cybersecurity solutions or produce critical-level hardware.