Document Type : Research Article
- Oleksandr Letychevskyi 1
- Yaroslav Hryniuk 1
- Viktor Yakovlev 1
- Volodymyr Peschanenko 2
- Viktor Radchenko 2
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.
 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.
 https://www.darpa.mil/program/cybergrand- challenge,, 2019.
 Alexander Letichevsky and David Gilbert. Interaction of agents and environments, 1999.
 http://apsystems.org.ua,, 2019.
 https://cve.mitre.org,, 2019.
 John Viega, M Howard, and D LeBlanc. Deadly sins of software security-programming flaws and how to fix them". 19.