Реплика: аудит исходных кодов и компиляторы

15. June 2010, 19:08 Безопасность, Компьютеры и ПО

Обсуждали тут аудит программного кода. Речь вот о чём: программное обеспечение, которое предназначено для решения каких-либо критичных задач, подвергают аудиту. Цели аудита: обнаружение возможных “закладок” и нехороших особенностей.

Для аудита можно использовать исходные коды. И их используют, потому что так удобнее. Есть разные автоматизированные инструменты и вообще – обкатанные подходы. Пример, который на слуху, аудит разработок Microsoft, для допуска к специальным компьютерам. Эта корпорация предоставляет исходники своих продуктов, на особых условиях.

Так вот, при обсуждении методов проверки “исходников” и получающихся результатов, нельзя забывать, что так же необходима проверка компиляторов и инструментов сборки исполняемых кодов. Если вы проверили “исходники” операционной системы (а там, кстати, миллионы строк) и ничего не нашли подозрительного, но при этом вообще не проверили компилятор, который эти исходники обрабатывает, то нельзя делать выводов об отсутствии закладок и дефектов – их может вносить компилятор.

Более того, известно, что вполне себе тщательно (но независимо) проверенный в “исходниках” компилятор, после применения к, опять же, проверенным исходным кодам, может дать на выходе (в исполняемом “бинарнике”) результат с неожиданными дырами и “закладками”. Добротный результат можно получить, если проверять совместно весь набор: и компилятор “в исходниках”, и “исходники” компилируемого продукта.

Да и собирать продукт вообще-то нужно самостоятельно (как с опенсорсными решениями и происходит). Очевидно, что в противном случае можно получить “немного не тот” исполняемый код. (Другой способ, менее эффективный: хитрый криптографический контроль сборки, проводимой на стороне разработчика ПО.)

(Часто озвучиваемая идея с подробной сверкой бинарного кода собственной сборки (из проверяемых исходников), и “оригинального” дистрибутива – особого смысла не имеет. Посудите сами: если вы и так можете получить идентичный “оригиналу” бинарный код, настаивать на использовании “оригинала” производителю смысла нет. Если же производитель что-то там, якобы, подписывает своими секретными ключами, и этим мотивирует изменение исполняемого кода, то особого доверия ко всей процедуре аудита уже быть не может.)

()

Похожие записки:



Далее - мнения и дискуссии

(Сообщения ниже добавляются читателями сайта, через форму, расположенную в конце страницы.)

Комментарии читателей блога: 27

  • 1. 15th June 2010, 19:35 // Читатель qehgt написал:

    Да вот же оно:

    http://stackoverflow.com/questions/781718/thompsons-trojan-compiler

    Именно так всё и работало.

  • 2. 15th June 2010, 19:57 // Читатель Stanislav написал:

    Ничего удивительного, в linuxtesting находили замечательные баги в стандартной библиотеке C, вроде значений синуса > 1.

  • 3. 16th June 2010, 00:06 // Читатель Z.T. написал:

    Компилятор C++ слишком сложная штука: понять что он создает bug который позволяет exploit очень трудно. Легче проверять готовый binary.

    Тема хорошо описана самим Томсоном в 1984 г.: http://cm.bell-labs.com/who/ken/trust.html

  • 4. 16th June 2010, 10:22 // Читатель Lim написал:

    А еще нужно проверять компиляторы, которыми компилировались исходники компилятора, и т.д. :)

  • 5. 16th June 2010, 13:00 // Читатель Sasha Nahayko написал:

    Насколько я помню, именно такая ситуация была описана в “Новом словаре хакера” Эрика С. Рэймонда, когда в исходный код компилятора был добавлен код, вставляющий черный ход для разработчика при компиляции некоторых программ, а так же код, который, при поступлении на вход компилятора его же исходного кода, вставлял в него при необходимости код, вставляющий… И змея кусала себя за хвост.

  • 6. 16th June 2010, 16:13 // Читатель sarin написал:

    любая проверка может имеет два возможных результата: нечто обнаружено и нечто не обнаружено. но никак не гарантию того, что нечто отсутствует.

    поэтому, я считаю, в критических областях следует больше внимания уделять созданию условий в которых наличие закладок или дыр не приведёт само по себе к образованию бреши в безопасности. безусловно какой-то аудит проводить нужно, но мне кажется, что с увеличением затрат на аудит его результативность будет увеличиваться хуже, чем линейно. при этом увеличение затрат на создание закладок будет куда более результативно.

    атакующая сторона (которая пытается разместить закладки) находится в существенно более выгодном положении. ведь она может использовать один из сотен (тысяч? сотен тысяч?) способов создать брешь в то время как атакуемая должна будет не только знать все возможные способы, что само по себе уже фантастично, но и проверить их.

  • 7. 16th June 2010, 17:19 // Александр Венедюхин ответил:

    Sarin, это всё так. Но всё ещё остаётся надежда, что через некоторое время нас спасёт доказательное программирование. Проблема тут из области прикладной математики. Сейчас пока затраты на доказательство свойств кода очень велики и себя не оправдывают на практике, но тема развивается.

  • 8. 16th June 2010, 18:49 // Читатель Z.T. написал:

    Пока formal proofs не практично, помогает http://en.wikipedia.org/wiki/Design_by_contract в виде аннотаций типа http://msdn.microsoft.com/en-us/library/ms235402.aspx

  • 9. 16th June 2010, 22:08 // Читатель kaschey написал:

    Для чего и разрабатывают .NET и сингулярити. Дыр для закладок будет на несколько порядков меньше. Сейчас закладки создаются без всякого злого умысла и даже при самом решительном им противодействии.

    С плюсами, конечно, так не выйдет, но для паскаля вполне реализуемо. Если обязать разработчика использовать только “доверенные” классы и конструкции (запретить арифметику указателей, прямое приведение типов), то можно существенно обезопасить код. В конце концов можно написать собственный интерпретатор, который проверяет код на безопасность.

  • 10. 17th June 2010, 03:43 // Читатель Jeff Zanooda написал:

    kasсhey, а как будет собственный интерпретатор проверять код на безопасность?

    Вот пример для тестирования:

    void testcase(int x, int y, int z, int n) {
    if (n>2 && pow(x,n)+pow(y,n)==pow(z,n)) payload();
    }

    Может вызваться закладка (функция payload) или нет? Этот же вопрос любителям доказательного программирования.

    pow(a,b) возводит a в степень b. Для простоты предположим, что без ошибок округления.

  • 11. 17th June 2010, 10:22 // Читатель sarin написал:

    Александр, я не силён в теории, но во втором томе Хорстмана я совершенно случайно вычитал что есть такая теорема что нельзя однозначно сделать никаких выводов о работе программы только на основании её кода. книжка сейчас на работе, точную формулировку наизусть не помню. каким образом доказательное программирование (совершенно не знаю что это такое) нарушит данную теорему?
    упоминание же теоремы у Хорстмана примечательно ещё и тем, что там рассматривается в контексте обеспечения безопасности в JVM.
    если найти место в программе где делается обращение к некоему хосту (вариант реализации бэкдора) порой не под силу даже тому кто это написал, то поймать программу за руку в тот момент когда она туда полезет не составляет ровным счётом никакого труда. появление и развитие технологии виртуальным машин обеспечило возможность для обеспечения полной безопасности работы совершенно неизвестного кода. прелесть данной концепции ещё и в том, что каждый параноик вполне может создать собственную виртуальную машину например для жавы. это, конечно, не простое дело, но вот не факт что сложнее подробного изучения кода хотя бы одной программы.

    Jeff Zanooda, пример очень хороший. но вот на основе изучения исходного кода я делаю вывод, что в программе присутствует вызов payload(). интересно же взглянуть, что там внутри.
    вообще когда я вижу чужой код (да чего греха таить, и свой иногда) у меня два состояния бывает. первое – я читаю и понимаю что тут делается и главное зачем, второе – не понимаю. если не понимаю, возникает внутреннее противоречие и острое желание переписать.

  • 12. 17th June 2010, 13:36 // Александр Венедюхин ответил:

    Sarin, я книгу не читал, но догадываюсь, что там, наверное, речь в книге о несколько другом: грубо говоря, нельзя написать программу, которая сможет определить завершится ли (всякая) другая программа, на основе анализа её кода и входных данных (halting problem).

    Доказательное программирование: это когда исходный код сопровождается доказательством отсутствия ошибок в нём. Совсем другая задача. Доказать можно, используя специально сконструированные формальные системы.

  • 13. 17th June 2010, 14:28 // Читатель sarin написал:

    доехал до работы и глянул: называется теоремой Гёделя.

    с доказательным программированием возникает та концептуальная проблема, что закладка не является ошибкой. понятно что всунуть бэкдор в код который должен быть тщательно документирован сложнее.

  • 14. 17th June 2010, 14:59 // Александр Венедюхин ответил:

    Ой, ну теорема Гёделя тут вообще ни при чём.

    Бекдор – вполне является ошибкой относительно условий на проект.

  • 15. 17th June 2010, 18:18 // Читатель sarin написал:

    представьте такую программу, которая заносит данные в базу. она подсчитывает количество занесённых записей и если оно превысило заданное (известно разработчикам) число то происходит перестройка индексов.

    каким образом доказательное программирование выявит бэкдор в этом, казалось бы, не хитром функционале?

  • 16. 17th June 2010, 18:32 // Александр Венедюхин ответил:

    Ну так это слишком общая формулировка: что за “база”, где она, что означает “заносит в базу”, что за индексы и т.д. Тут столько вариантов, что, конечно, не поможет доказательное программирование, которое имеет дело с конкретными исходными кодами и специальными формальными системами.

  • 17. 17th June 2010, 20:02 // Читатель sarin написал:

    вот такая может быть атака например: построение индекса в РСУБД относительно затратная операция. если условный противник получит возможность наблюдать за энэргопотреблением сервера где работает СУБД, то теоретически сможет узнать что количество новых записей превысило N.

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

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

    это, конечно, паранойя. но и мир жесток.

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

  • 18. 17th June 2010, 20:13 // Читатель Jeff Zanooda написал:

    Ну хорошо, скажем вместо payload() error(). Смысл от этого не меняется – это то, что программа делать не должна.

    Как доказательное программирование и умные компиляторы будут определять, может ли при каких-то условиях эта программа делать то, что не должна, или нет? У Перельмана спросят?

  • 19. 17th June 2010, 21:55 // Читатель sarin написал:

    Jeff, мне никакого программирования вообще не надо, чтобы заявить, что при x, y, z = 0 при любом n > 2 вызовется закладка. но я не могу знать могут ли такие x, y, z придти на вход. разумеется если я провожу аудит на предмет безопасности то “может” автоматически заменяется на “обязательно”. и даже если я увижу
    if (false){
    украстьСамыйСекретныйДокумент();
    }
    то сочту что программа содержит закладку.

  • 20. 17th June 2010, 22:03 // Читатель Jeff Zanooda написал:

    То есть доказательное программирование основано на анализе названий функций? А если я переименую функцию украстьСамыйСекретныйДокумент() в processData()? А если я добавлю ограничение, что x, y, z больше нуля?

  • 21. 17th June 2010, 23:01 // Читатель sarin написал:

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

    если аудитор находит непонятный для него код он должен забить тревогу.

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

  • 22. 18th June 2010, 01:24 // Читатель Z.T. написал:

    Про закладки: http://en.wikipedia.org/wiki/Underhanded_C_Contest

    Насчет индекса RDBMS, если надо то формальными методами построят data structure который гарантируя минимальные требования по throughput (IOPs) еще и обеспечивает latency, то есть не имеет редкого но возможно длительного периода реорганизации как скажем B+Tree. Конечно, это понизит средний ожидаемый throughput, но раз надо – так надо. Тот же trade-off как pause-less garbage collection: гарантия latency ценой throughput. Похоже на то как криптографические алгоритмы выполняются так чтобы длительность времени не зависела от данных: медленней но с меньшей утечкой информации.

  • 23. 18th June 2010, 07:51 // Читатель sarin написал:

    так ведь знать ещё нужно что надо

  • 24. 20th June 2010, 15:28 // Читатель kaschey написал:

    Jeff Zanooda: а как будет собственный интерпретатор проверять код на безопасность?

    Я писал про паскаль, который как и .NET может обеспечить безопасность кода. Для технологии .NET атаки на переполнение буфера невозможны в принципе. Для Delphi только при намеренном внедрении таких дыр программистом. Для С++ переполнение буфера это неизбежное зло.

    Задав программе на .NET определённый уровень полномочий можно не беспокоиться об их нарушении, этого не допустит среда .NET.

    Атаковать браузер написанный на .NET невозможно. Атаковать паскалевский браузер возможно только теоретически (и при злом умысле программиста). С++ браузеры атакуют бесконечно и никто не может толком закрыть дыры несмотря на все усилия.

  • 25. 20th June 2010, 16:27 // Читатель Jeff Zanooda написал:

    А почему невозможно атаковать браузер, написанный на .NET? Потому что он не существует?

    Безопасность кода – это не только и не столько отсутствие переполнений буфера. С этой проблемой как раз есть способы бороться: инструментарий вроде Valgrind, поддержка со стороны операционной системы типа stack execution protection, программирование в C++ на языке C++ (а не C).

    Посмотрите на то, какие дыры в безопасности чаще всего находят в современных программах. Это XSS, неправильная обработка спец символов вроде кавычек во входных данных, оставленные “на всякий случай” люки для отладки. Язык тут вообще не при чём.

    Если код победителя упомянутого выше Underhanded C Contest перевести на C#, думаете, он перестанет работать?

  • 26. 21st June 2010, 13:08 // Читатель sarin написал:

    программа написанная на .Net исполняется контролируемо. можно ограничить ей права на работу с файловой системой, ограничить сетевую активность и т. д. в жаве это всё точно есть.

    другое дело, что серьёзным программам нужны серьёзные права и единожды их получив злая программа может сделать свои чёрные дела.

  • 27. 21st June 2010, 15:00 // Читатель kaschey написал:

    Jeff Zanooda: “Безопасность кода ? это не только и не столько отсутствие переполнений буфера”

    Это самая серьезная и показательная из дыр. Никакие спец-инстркменты никогда не закроют эту дыру в Си насегда (тем более их почти не используют). Лучше язык и среда в которых этого не может быть в принципе.

    “неправильная обработка спец символов вроде кавычек во входных данных”

    Это дыры HTML. HTML по дыро-лояльности ушёл на сто шагов вперед от Си. Для меня до сих пор уивительно, что его и не пытаются заменить чем-то более современным, а только усложняют.