Тестирование безопасности программного обеспечения на языке С с использованием верификатора SPIN

The C language is widely used for developing tools in various application areas, and a number of C software tools are used for critical systems, such as medicine, transport, etc. Correspondingly, the security of such programs should be thoroughly tested, i.e., it is important to develop techniques for detecting vulnerabilities in C programs. In this paper we present an approach for dynamic detection of software vulnerabilities using the SPIN model checker. We discuss how this approach can be implemented in order to detect automatically C code vulnerabilities and illustrate a proposed technique for a number of C programs which are widely used in a number of applications.Предлагается метод тестирования безопасности С программ с использованием широко известного верификатора SPIN. Обсуждаются классы уязвимостей в С программах, которые могут быть обнаружены с использованием предложенного подхода. Приводятся результаты компьютерных экспериментов по обнаружению уязвимостей в студенческих программных реализациях алгоритмов работы с массивами