Comments 4
Всегда было очень интересно как можно формально верифицировать код на с/с++
Много на прошлой работе теоретизировали насчёт это верификации, но до дела так и не добрались.
ИМХО, метод формальной верификации языка с UB тянет на несколько нобелевских премий
Event-B и подобные — это формальная верификация модели, а не кода. С точки зрения продукта это проверка требований, выраженных в терминах модели, а не того, как они реализованы. Очевиден разрыв между тем, что смоделировано, и кодом, который будет реально пытаться это сделать.
Полнота модели — это не только не включить лишнее, но и не упустить важное (если мы хотим, чтобы модель была реально полезной). Например, что пользователь не должен быть способен сделать то, на что у него нет прав — очевидный инвариант безопасности в модели контроля доступа. Но вот в системе есть механизм повышения прав (как UAC в Windows). Можно сделать модель как положено: с эффективными и допустимыми правами, с действием повышения прав; инвариант будет, что эффективные права не могут выходить за рамки допустимых. А можно ограничиться текущим набором прав и не выдвигать инварианта, что текущий набор не может стать шире начального, потому что может же легальным образом. Даже если модель все учитывает, можно просто забыть проверит все нужные свойства. В результате к формальному доказательству нужно неформальное пояснение, что мы доказываем и почему (и как — бывают неочевидные преобразования).
Я делал модель безопасности на Event-B для сертификации ФСТЭК. Делал на совесть и это было очень интересно, но это не помогло найти ошибок и описание не получилось строже и понятнее документации.
Формальная верификация в информационной безопасности. Как пройти сертификацию во ФСТЭК