Control Systems and Computers, N6, 2019, Article 1
https://doi.org/10.15407/csc.2019.06.005
Control Systems and Computers, 2019, Issue 6 (284), pp. 5-20.
UDK 004.05, 004.4[2+9], 004.94, 519.7
O.O. Letychevskyi, Doctor (Phys.-Math.), Head of department, V.M. Glushkov Institute of Cybernetics of NAS of Ukraine, Glushkov ave., 40, Kyiv, 03187, Ukraine,
oleksandr.letychevskyi@garuda.ai
Ya.V. Hryniuk, Ph.D. student of Computer Science at V.M. Glushkov Institute of Cybernetics of NAS of Ukraine, Glushkov ave., 40, Kyiv, 03187, Ukraine,
yaroslav.hryniuk@garuda.ai
V.M. Yakovlev, Lead Mathematician at V.M. Glushkov Institute of Cybernetics of NAS of Ukraine, Glushkov ave., 40, Kyiv, 03187, Ukraine, victoryakovlev@ukr.net
ALGEBRAIC APPROACH TO VULNERABILITIES
FORMALIZATION IN THE BINARY CODE
Introduction. The security and protection of the software resources is one of the most current problem in the IT industry nowadays. The approaches to the threat modeling and vulnerabilities detection, based on the symbolic methods, became 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.
Purpose. Although the symbolic modeling could be effectively used for the code vulnerabilities detection, the relevant software tools are very slow. Also, the reachability problem during the symbolic programme execution is unresolvable in the common case. In the article, the formalization of representation of binary code and vulnerabilities based on the behavior algebra, and an approach that allow speeding up the vulnerabilities search, and reducing the area of the symbolic modeling 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.
Methods. 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.
Results. The methodology of development of the vulnerabilities description in the terms of the behavior algebra has been proposed. The algebraic matching algorithm has been implemented in the scientific prototype system, which has been successfully used to check several programmes for the known vulnerabilities.
Conclusion. 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.
Download full text! (On Ukrainian)
Keywords: software vulnerabilities, symbolic modeling, algebraic matching, behavior algebra.
- DARPA, “Cyber Grand Challenge.” [Online]. Available at:<https://www.cybergrandchallenge.com> [Accessed 21 Oct. 2018].
- Cha, S.K., Avgerinos, T., Rebert, A. and Brumley, D., 2012. “Unleashing Mayhem on binary code,” Proc. of IEEE Symposium on Security and Privacy, pp. 380-394.
https://doi.org/10.1109/SP.2012.31 - Nguyen-Tuong, Melski, J. W. Davidson, M. Co, W. Hawkins, J. D. Hiser, D. Morris, D. Nguen, and E. Rizzi, 2008.”Xandra: An autonomous cyber battle system for the Cyber Grand Challenge,” IEEE Security & Privacy, vol. 16 , no. 2, pp. 42-53.
https://doi.org/10.1109/MSP.2018.1870876 - Mechaphish, “Github repository.” [Online]. Available at:<https://github. com/mechaphish/mecha-docs> [Accessed 21 Oct. 2019].
- Gilbert, D., Letichevsky, A., 1999. “Interaction of agents and environments,” Recent trends in algebraic development technique, LNCS 1827, Springer-Verlag.
https://doi.org/10.1007/978-3-540-44616-3_18 - Algebraic Programming System, APS, [Online]. Available at:<www.apsystem.org.ua> [Accessed 2 Oct. 2019].
- Howard, M., LeBlanc, D., Viega, J., 2010. 24 Deadly Sins of Software Security: Programming Flaws and How to Fix Them. McGraw-Hill.
- Letychevskyi, O. and Letichevsky, A., 2012. “Predicate transformers and system verification”. Proc. Third International Workshop on Symbolic Computation in Software Science (SCSS 2010).
- Matt Conover & OdedHorovitz. Reliable Windows Heap Exploits. [Online]. Available at:<http://xcon.xfocus.org/XCon2004/archives/14_Reliable%20Windows%20Heap%20Exploits_BY_SHOK.pdf> [Accessed 2 Oct. 2019].
Received 14.11.2019
