DOI: https://doi.org/10.15407/pp2020.01.047

Algebraic patterns of binary code vulnerabilities

V.M. Yakovlev

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


Keywords


software vulnerabilities; symbolic modeling; algebraic matching; behavior algebra

Full Text:

PDF (Ukrainian)

References


DARPA, "Cyber Grand Challenge." [Online]. Available: https://www. cybergrandchallenge.com/.

Cha S.K., Avgerinos T., Rebert A., Brumley D., "Unleashing Mayhem on binary code," Proceedings. IEEE Symposium on Security and Privacy. 2012. P. 380-394. CrossRef

Nguyen-Tuong A., Melski D., Davidson J.W., Co M., Hawkins W., Hiser J.D., Morris D., Nguen D., and Rizzi E. "Xandra: An autonomous cyber battle system for the Cyber Grand Challenge," IEEE Security & Privacy. 2008. Vol. 16. N. 2. P. 42-53. CrossRef

Mechaphish, "Github repository." [Online].

Available from:https://github.com/mechaphish/mecha-docs.

Chipounov V., Kuznetsov V., Candea G. "S2E: A platform for invivo multi-path analysis of software systems." Asplos. 2011. Vol. 46. P. 1-14. CrossRef

Sen K., Marinov D., Agha G., Sen K., Marinov D., Agha G. "CUTE: A concolic unit testing engine for C." 10th European Software Engineering Conference and 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE'05). 2005. Vol. 30. N. 5. P. 263. CrossRef

Cadar C., Dunbar D., Engler D.R. "KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs," Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 2008. P. 209-224.

Gilbert D., Letichevsky A. "Interaction of agents and environments," Recent trends in algebraic development technique, LNCS 1827 (D. Bert and C. Choppy, eds.), Springer-Verlag, 1999.

Intel 64 and IA-32. "Architectures software developer's manual." Intel Corporation. 1997-2016.

Algebraic Programming System, APS, [Online]. www.apsystem.org.ua




DOI: https://doi.org/10.15407/pp2020.01.047

Refbacks

  • There are currently no refbacks.