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 Glushkov Institute of Cybernetics of National Academy of Sciences of Ukraine 40, Glushkova prospect, Kyiv, Ukraine
3 Garuda AI B.V., 54-62, Beachavenu, Schiphol-Rijk, Netherlands
4 Glushkov Institute of Cybernetics of National Academy of Sciences of Ukraine 40, Glushkova prospect, Kyiv, Ukraine
5 Garuda AI B.V., 54-62, Beachavenu, Schiphol-Rijk, Netherlands
doi
10.22042/isecure.2019.11.0.1چکیده
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.
