Automated Assertion Checker Generator and Information Flow Tracking for Security Verification

Miguel Alfaro Zapata, Amirhossein Shahshahani, Zeljko Zilic
McGill University


The increasing complexity of designs and the emergence of hardware security vulnerabilities pose challenges to efficient verification. This paper presents an automated tool that integrates Information Flow Tracking (IFT), automated assertion generation, and hardware assertion checkers to detect information leakage vulnerabilities on hardware designs. The tool generates tagged RTL models using IFT techniques and automatically generates security assertions based on specified secure assets. The security assertions are then converted into hardware assertion checkers. The tool was evaluated on various RTL designs, and the impact on FPGA resource utilization was measured. The results show that our tool successfully generates security assertions and assertion checkers, providing a systematic approach to security verification in hardware designs.