На факультете вычислительной математики и кибернетики МГУ создали метод, ускоряющий анализ программ на наличие ошибок и уязвимостей. Результаты были представлены в рамках конференции «Ломоносовские чтения».

Статический анализ позволяет проверять программное обеспечение без запуска программы. В процессе формируются логические условия, которые описывают возможные значения переменных в различных точках программы. При изучении различных путей выполнения алгоритма такие условия быстро усложняются и увеличиваются в размере. Это делает процесс медленнее, увеличивает потребление памяти и снижает масштабируемость при работе с большими программными проектами.

В работе рассматриваются методы упрощения таких условий, реализованные в статическом анализаторе SharpChecker, входящем в состав системы анализа программ Svace. Предложен метод подстановок, позволяющий упрощать логические формулы, возникающие в процессе символьного выполнения программы. Использование равенств между выражениями позволяет заменять переменные и уменьшать сложность логических условий.

Кроме того, разработана многоуровневая система упрощения формул. Она применяется по мере построения новых условий и включает выявление противоречивых ограничений, применение преобразований на основе законов булевой алгебры и эвристические ограничения сложности формул.

«Одним из ключевых элементов системы является метод подстановок. Он позволяет использовать равенства между выражениями для упрощения других ограничений внутри предикатных формул и тем самым уменьшать их сложность при статическом анализе программ», — отметил доцент кафедры системного программирования факультета ВМК МГУ Валерий Игнатьев.