BONC: a framework for automatic cryptanalysis using the implementation code

Abstract The security analysis of symmetric ciphers is a time-consuming and labor-intensive process that traditionally relies on manual derivation and mathematical modeling for specific algorithms. This paper introduces a fully automated analysis software framework designed to evaluate the security of any round-based symmetric cipher constructed from common primitives like S-boxes, bit permutations, and XOR operations. Our approach leverages the LLVM compiler infrastructure and the KLEE symbolic execution engine to automatically convert C implementations of cryptographic algorithms into a structured representation of state bits and update functions. By employing a frontend that uses custom annotations to identify round functions, it translates the algorithm into a series of Bit Expressions, and we introduce multiple modular backends that process those Expressions to applicable form of performing various types of analyzing methods. We demonstrate the tool’s effectiveness by implementing a differential and linear cryptanalysis backend with help of SAT solver, Division Property integral cryptanalysis backend with help of MILP solver, and a degree estimation backend based on Numeric Mapping method. As an experimental result, we apply these automated analysis techniques to several finalists from the NIST Lightweight Cryptography (LWC) competition, successfully reproducing and improving some existing cryptanalytic results. This work significantly lowers the barrier for cryptographic research by providing a powerful and adaptable platform for automatically assessing the security of both existing and newly designed symmetric ciphers.