Algebraic Matching of Vulnerabilities in a Low-Level Code


1 Glushkov Institute of Cybernetics of National Academy of Sciences of Ukraine 40, Glushkova prospect, Kyiv, Ukraine

2 Garuda AI B.V., 54-62, Beachavenu, Schiphol-Rijk, Netherlands



This paper explores the algebraic matching approach for detection of vulnerabilities in binary codes. The algebraic programming system is used for implementing this method. It is anticipated that models of vulnerabilities and programs to be verified are presented as behavior algebra and action language specifications. The methods of algebraic matching are based on rewriting rules and techniques with usage of conditional rewriting. This process is combined with symbolic modeling that gives a possibility to provide accurate detection of vulnerabilities. The paper provides examples of formalization of vulnerability models and translation of binary codes to behavior algebra expressions.


[1] Marco Cova, Viktoria Felmetsger, Greg Banks, and Giovanni Vigna. Static detection of vulnerabilities in x86 executables. In 2006 22nd Annual Computer Security Applications Conference (ACSAC’06), pages 269–278. IEEE, 2006.
[2] Maryam Mouzarani, Babak Sadeghiyan, and Mohammad Zolfaghari. Detecting injection vulnerabilities in executable codes with concolic execution. In 2017 8th IEEE International Conference on Software Engineering and Service Science (ICSESS), pages 50–57. IEEE, 2017.
[3] challenge,, 2019.
[4] Alexander Letichevsky and David Gilbert. Interaction of agents and environments, 1999.
[5],, 2019.
[6],, 2019.
[7] John Viega, M Howard, and D LeBlanc. Deadly sins of software security-programming flaws and how to fix them". 19.