Algebraic patterns of binary code vulnerabilities

Abstract

Detection of software systems’ vulnerabilities is an actual problem in the IT industry nowadays. The approaches to the solution of this problem, based on the symbolic methods, became very popular and promising during the last decade. The article describes an approach to the vulnerabilities detection in the binary code, based on the formal methods of symbolic modeling and algebraic matching. In the article, the formalization of representation of binary code and vulnerabilities based on the behavior algebra, and the method of creation of formal patterns of vulnerabilities are proposed. The behavior algebra used for the representation of the formal binary code behavior, as well as for describing the vulnerabilities behavior. However, while the representation of the binary code in the terms of behavior algebra could be automated, creation of the vulnerabilities description requires development of the correct and effective methodology. Using the behavior algebra representation, the task of vulnerabilities detection can be solved in two steps – relatively fast algebraic matching, and the symbolic modeling itself, based on the data provided by the algebraic matcher. By the development of the vulnerabilities description in the terms of behavior algebra, and the algebraic matching algorithm the speed of detection of vulnerabilities in the binary code can be increased. The methodology of development of the vulnerabilities description in the terms of the behavior algebra has been proposed. The advantage of the algebraic approach is that the code vulnerabilities can be found more precisely, and the vulnerability description in the terms of behavior algebra can take in account different possible kinds of it. Also, the experiments with the implementation prototype shown that the “two-level” vulnerability detection system is faster than “pure” symbolic modeling: the fast matching step is executed first, and the slow modeling step is executed next on the results, provided by the matching step.

Prombles in programming 2020; 1: 47-54