Теорема Пифагора

[arkenoi]

Когда-то давно, в 90-е годы, когда интернет был еще маленьким и каким-то "игрушечным", Internet Explorer'а не существовало в природе, слово "дотком" еще толком ничего толком не значило, все интересующиеся безопасностью, конечно, до дыр зачитывали Оранжевую Книгу. Конечно, священный терпет вызывала система Gemini, единственная и последняя сертифицированная аж по уровню A1, круче которого не может быть даже яйцо динозавра сваренное в жерле вулкана. Ве-ри-фи-ци-ро-ванная безопасность! Математически доказанная! Эти слова вызывали в воображении образы полностью контролируемого (начиная с нисхождения нетварного огня, не иначе) технологического процесса производства Совершенно Особенного оборудования и священнодействие "полной алгоритмической верификации" всего софта начиная с микрокода процессора. Как это может быть, никто себе толком не представлял, но все Уверовали.

Никто даже не мечтал проникнуть в Священные Тайны далее, ибо Коком.

Шли годы. Коком рассосался. url на двери общественного туалета стал сначала поводом для юмористических картинок, а затем - обыденной реальностью. Оранжевая книга превратилась в Common Criteria. Уровень A1/EAL7 остался все за тем же единственным лидером! Развивался интернет, появился и лопнул пузырь доткомов, худо-бедно какую-то сертификацию уже не в столь комической конфигурации, как поначалу, получил даже MS Windows. И вот, оказывается, в 2003 году Gemini Computers была приобретена компанией Aesec. Которая, наконец-то, позволила простым смертным ознакомиться с тем, как именно Gemini решили, казалось бы, принципиально неразрешимую задачу о невозможности обнаружения закладки в компиляторе. Как им удалось алгоритмически верифицировать компилятор?!

На сайте есть кучка презентаций, pdf'ок и в них - ответ на этот вопрос. И на многие другие. Как? Да очень просто. У них был компилятор, разработка которого проводилась, ну типа, под некоторым контролем. Вот его "приказом по лагерю" назначили доверенным. Ну и дальше можно тащить себя за волосы из болота.

-- Гоги, докажи что квадрат гипотэнузы равэн сумме квадратов катэтов?
-- Вах, учитэл, мамой клянус!

Вот примерно так. А специальное доверенное железо постороено на серийных x86 процессорах и других обычных китайских комплектующих. Да и собирается, небось, тоже в Китае.
Сама система построена хорошо, разумно, но ничем принципиально не отличается от обычных B-level систем или от российского "Феникса" (которого, впрочем, толком не бывает).

А чудес не существует.

Comments

[blacklion.livejournal.com]

А что за "Феникс"?

[arkanoid.livejournal.com]

http://www.ssl.stu.neva.ru/fenix/index.html

большая часть линков битые, предупреждаю. но оно есть в природе и даже грузиццо ;-)

[blacklion.livejournal.com]

Я бы сказал — все битые :)
А на что оно похоже для программиста? POSIX экспортит на application layer?

[arkanoid.livejournal.com]

Фрагментарно. Но самбу, вроде, портировать смогли.

[pustota1.livejournal.com]

Командир, ты чего то не то курил сегодня. А как же SCOMP известной вентиляторной фирмы Honeywell? Ну, и в ревущее 90-ые все прочли и Reflections on Trusting Trust -- не обаружение закладки в компайлере представляет неразрешимую задачу, просто надо осознавать где ты готов остановиться в поиске этой закладки.

[http://users.livejournal.com/_qwerty/]

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

[pustota1.livejournal.com]

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

[http://users.livejournal.com/_qwerty/]

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

[pustota1.livejournal.com]

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

[http://users.livejournal.com/_qwerty/]

С точки зрения теории нет разницы между теорией и практикой.

[halina.livejournal.com]

21 сентября, в пятницу в 19:15, в киноклубе будет фильм-легенда немецкого режиссера Вима Вендерса "Небо над Берлином" (1987).

Адрес киноклуба:
Проспект Мира, дом 26 строение 1, вход с Грохольского переулка.
Ищите стекляную дверь с надписью "Администрация Ботанического сада МГУ", в дальнем относительно Проспекта Мира конце красного кирпичного здания.
Сообщите охраннику, что Вы пришли в киноклуб.
Далее поднимайтесь по лестнице на 2й этаж в лабораторию.

[arkanoid.livejournal.com]

Спасибо! Я его видел, конечно, но в хорошей компании с удовольствием посмотрю еще раз ;-)

[halina.livejournal.com]

Я пока совершенно ничего не знаю про свою пятницу. :(

[arkanoid.livejournal.com]

Ну, ближе к - поймем..

[e1am0.livejournal.com]

я занимался этой проблемой. в смысле доверенным компилятором(средством разработки). не буду кичиться своим высоким интеллектуальным уровнем или какими-то научными подвигами. чего нет, того нет.
но по теме мной было предложено только 2 возможных варианта:
1. это спиральная разработка под присмотром с чёткой и жёсткой технологией.
2. вознеся молитву аллаху, надеяться, что мульярд леммингов пользователей и разработчиков опенсорс не могу ошибаться и юзать опенсорсные программы.
разница между двумя подходами - во втором случае отложенные расходы, причём размер их оценить невозможно. ибо это вопрос ВЕРЫ ))))

[ex-ivlad.livejournal.com]

я не видел живого человека (кроме себя), который заглядывал в сорцы GnuPG. а казалось бы.

[e1am0.livejournal.com]

поэтому я выделил слово ВЕРА. Надо верить, что они есть, ибо их наличие подтверждается косвенными признаками.

ЗЫ. На самом деле все мы в матрице, поэтому данная словестная полемика не имеет смысла )))