Комментарии 11
Могли внести уязвимости целенаправленно?
НЛО прилетело и опубликовало эту надпись здесь
Пора переписывать на Rust? Вон уже есть подобное — https://github.com/ctz/rustls
С другой стороны… OH, WAIT, SHI~
Там же наверняка сам бинарный API несовместим и дыряв. И что делать с теми ребятами, которые хотят статически линковаться… С другой стороны — rust же поверх llvm? значит, можно что-то придумать
Там ошибка не в реализации, а в логике. Вроде, такое должно тестами крыться.
НЛО прилетело и опубликовало эту надпись здесь
В принципе соглашусь — то, что там Си, который только ленивый не знает — не способствует нахождению ошибок или их исправлению. Не всякий может контрибьютит, а тот, кто может, не факт, что может делать это хорошо.
Поэтому — да, давайте перепишем на идрис
Возникают вопросы о таком подходе. Хотелось бы понять, как на них отвечать.
- Если обложить всё типами, то как решать проблему с производительностью? Если доказывать с nat в стиле Пеано, можно попрощаться с производительностью, а она важна для массовой криптографии. Формально доказывать что-то про модулярную быструю арифметику крайне трудозатратно. Microsoft потратила уйму средств и времени для доказательства простой арифметической оптимизации.
- Почему ошибки на уровне спецификации будет проще обнаружить, чем ошибки на уровне самого кода?
НЛО прилетело и опубликовало эту надпись здесь
Проблема может быть в том, что в gmp может не быть ошибок, но модель библиотеки не верная (такое было, например, в CompCert с описанием архитектуры Power). Проблема не в том, что формулы не корректные логически, а в том, что они не отражают реальность. Условно: механика Ньютона не противоречива, но обсчитывать на её основе Глонасс невозможно.
Не условно: вот есть мандатные политики безопасности. Это когда права доступа задают решётками в которых есть вполне естественные требования: нельзя читать «сверху» и нельзя писать «вниз». Можно формализовать эти ограничения, а потом перевернуть решётку, и ничего в корректности не поменяется, только ограничения уже будут иными: нельзя читать «снизу», нельзя писать «вверх». С точки зрения безопасности — это нонсенс. Но тем не менее, я видел статью, в которой за корректное поведение выдаётся именно это, и это же и доказывается.
В этом нет логических противоречий, но, как очевидно, это огромная дыра в безопасности.
Как быть с такими ситуациями? Зная такие особенности, по идее, я всё-равно, должен буду независимо проверить предлагаемый мне исходный код. По идее, я могу пойти и прочитать все спецификации, но в реальных проектах их офигенно много, тысячи, не сотни. Более того, культура верифицирующего сообщества такова, что комментарии и пояснения к спецификациям люди не пишут. Названия лемм легко могут быть малопонятными, типа: pqq_is_ttnm. И так далее, и тому подобное. Часто встречаются самописные тактики, которые в Coq, например, плохо изолированы от ядра.
Я много раз пробовал читать «промышленные» верификации, и не разу ещё не смог разобраться в структуре.
И что мне со всем этим делать? Получается, что только тестировать своими тестами. А раз, всё равно, я должен тестировать, то в ту ли технологию были вложены силы разработчиков?
Ну, и производительность важна. В конце концов, мы используем компьютеры не только по той причине, что они точно воспроизводят инструкции, но и по той причине, что они делают это быстро. Если проверка сертификата будет занимать несколько минут, насколько дороже станут платежи в интернете или банковское обслуживание? Если реконструкция МРТ-снимка будет занимать недели (а с float-ами доказывать ещё сложнее, чем в кольцах вычетов, поэтому доказывают не для float-ов, а для рациональных чисел), сколько пациентов не удастся спасти?
Такие вот у меня сомнения.
P.S. О тестах. Я не утверждаю, что тесты лучше. Но они объективно проще, во-первых. А, во-вторых, структура ПО может быть отвязана от структуры тестов, в отличии от доказательств, где важна структура самого исполняемого кода. Значит, разнообразных тестов можно навешать больше, этим сможет заняться больше людей. Тесты могут быть связаны с реальной аппаратурой и внешним миром. И их тоже можно обрабатывать методами абстрактной интерпретации, считая код доказательством этих тестов.
В чём я ошибаюсь?
Не условно: вот есть мандатные политики безопасности. Это когда права доступа задают решётками в которых есть вполне естественные требования: нельзя читать «сверху» и нельзя писать «вниз». Можно формализовать эти ограничения, а потом перевернуть решётку, и ничего в корректности не поменяется, только ограничения уже будут иными: нельзя читать «снизу», нельзя писать «вверх». С точки зрения безопасности — это нонсенс. Но тем не менее, я видел статью, в которой за корректное поведение выдаётся именно это, и это же и доказывается.
В этом нет логических противоречий, но, как очевидно, это огромная дыра в безопасности.
Как быть с такими ситуациями? Зная такие особенности, по идее, я всё-равно, должен буду независимо проверить предлагаемый мне исходный код. По идее, я могу пойти и прочитать все спецификации, но в реальных проектах их офигенно много, тысячи, не сотни. Более того, культура верифицирующего сообщества такова, что комментарии и пояснения к спецификациям люди не пишут. Названия лемм легко могут быть малопонятными, типа: pqq_is_ttnm. И так далее, и тому подобное. Часто встречаются самописные тактики, которые в Coq, например, плохо изолированы от ядра.
Я много раз пробовал читать «промышленные» верификации, и не разу ещё не смог разобраться в структуре.
И что мне со всем этим делать? Получается, что только тестировать своими тестами. А раз, всё равно, я должен тестировать, то в ту ли технологию были вложены силы разработчиков?
Ну, и производительность важна. В конце концов, мы используем компьютеры не только по той причине, что они точно воспроизводят инструкции, но и по той причине, что они делают это быстро. Если проверка сертификата будет занимать несколько минут, насколько дороже станут платежи в интернете или банковское обслуживание? Если реконструкция МРТ-снимка будет занимать недели (а с float-ами доказывать ещё сложнее, чем в кольцах вычетов, поэтому доказывают не для float-ов, а для рациональных чисел), сколько пациентов не удастся спасти?
Такие вот у меня сомнения.
P.S. О тестах. Я не утверждаю, что тесты лучше. Но они объективно проще, во-первых. А, во-вторых, структура ПО может быть отвязана от структуры тестов, в отличии от доказательств, где важна структура самого исполняемого кода. Значит, разнообразных тестов можно навешать больше, этим сможет заняться больше людей. Тесты могут быть связаны с реальной аппаратурой и внешним миром. И их тоже можно обрабатывать методами абстрактной интерпретации, считая код доказательством этих тестов.
В чём я ошибаюсь?
Остальные ошибки пока ещё не нашли.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
В OpenSSL нашли две опасные уязвимости