Verification of LLVM bit-code via a system of Constrained Horn Clauses

Abstract

Diplomová práca predstavuje nový nástroj na statickú verifikáciu programov s názvom Hornix. Hlavným cieľom je overenie základných tvrdení o stave premenných a dosiahnutých stavoch programu. Základným stavebným kameňom nástroja je projekt LLVM a jeho infraštruktúra kompilátora (LLVM Compiler Infrastructure), ktorá sa používa na preklad programu zo zdrojového kódu do medzikódu, nazývaného LLVM Intermediate Representation (LLVM IR). Nástroj následne využíva optimalizačnú infraštruktúru LLVM (LLVM Pass Infrastructure) na transformáciu medzikódu do modelu reprezentovaného pomocou Constrained Horn Clauses (CHC). Splniteľnosť modelu je rozhodovaná pomocou jedného z existujúcich riešičov CHC. Hornix bol testovaný na testovacej sade SV-Benchmarks, kde úspešne overil bezpečnosť veľkého množstva zadaní. Výsledky však zároveň ukázali, že pri mnohých zadaniach došlo k prekročeniu stanoveného časového limitu na výpočet. Nástroj Hornix bol tiež zapojený do medzinárodnej súťaže zameranej na verifikáciu softvéru, SV- COMP 2025, kde obsadil 4. miesto z 26 účastníkov v kategórii ReachSafety-Recursive.

The master thesis presents a novel static software verification tool, Hornix. The primary goal of the tool is to verify basic assertions concerning variable states and program execution paths. The tool is built upon the LLVM Project, utilizing the LLVM Compiler Infrastructure to translate source code into LLVM Intermediate Representation (LLVM IR) and the LLVM Pass Infrastructure to transform these instructions into Constrained Horn Clauses (CHC). The generated CHC model represents the program, and its satisfiability is determined using external CHC solvers. Hornix was evaluated on a subset of SV- Benchmarks, where it successfully verified program safety in a significant number of cases. However, the results also revealed several benchmarks that could not be resolved within a reasonable time frame. Additionally, Hornix participated in the international competition SV-COMP 2025, achieving 4th place out of 26 participants in the ReachSafety-Recursive category, demonstrating its potential as an effective tool for software verification despite areas needing improvement.