Формальные методы в C ++ для безопасного программного обеспечения
Глядя на C, C имеет хорошую поддержку формальных методов, которые могут использоваться в коде (frama-c, VCC, Verifiedast). Насколько я могу судить, в C ++ нет ничего похожего.
Какие формальные методы доступны для рассуждения о безопасности программного обеспечения, написанного на C ++?
Решение
Медицинская компания, с которой я работаю Coverity а также Klocwork проверить код на наличие возможных проблем, таких как утечка ресурсов и использование неинициализированного указателя.
Тем не менее, это инструменты, которые не являются стандартными для критического кода безопасности.
Что я видел, так это то, что MISRA работает над стандартом для C ++. Они начали с C и начали работать над C ++ около 5 лет назад. Одна большая проблема заключается в том, что стандарт MISRA для C ++, например, говорит, что вы не должны использовать шаблоны. Это действительно ограничивает то, что вы можете сделать в C ++. Тем не менее, вы можете использовать этот документ в качестве отправной точки. Вы можете захотеть ограничить шаблоны, используемые в вашем программном обеспечении, к тому, что входит в стандартную библиотеку и повысить, например.
Обратите внимание, что Klocwork имеет расширение для MISRA C ++.
Тем не менее, один из лучших способов написать хороший код — это проверить его с помощью модульных и интеграционных тестов. С годами я обнаружил, что это гораздо надежнее, чем большинство других методов.
Другие решения