Теорема Пифагора
Когда-то давно, в 90-е годы, когда интернет был еще маленьким и каким-то "игрушечным", Internet Explorer'а не существовало в природе, слово "дотком" еще толком ничего толком не значило, все интересующиеся безопасностью, конечно, до дыр зачитывали Оранжевую Книгу. Конечно, священный терпет вызывала система Gemini, единственная и последняя сертифицированная аж по уровню A1, круче которого не может быть даже яйцо динозавра сваренное в жерле вулкана. Ве-ри-фи-ци-ро-ванная безопасность! Математически доказанная! Эти слова вызывали в воображении образы полностью контролируемого (начиная с нисхождения нетварного огня, не иначе) технологического процесса производства Совершенно Особенного оборудования и священнодействие "полной алгоритмической верификации" всего софта начиная с микрокода процессора. Как это может быть, никто себе толком не представлял, но все Уверовали.
Никто даже не мечтал проникнуть в Священные Тайны далее, ибо Коком.
Шли годы. Коком рассосался. url на двери общественного туалета стал сначала поводом для юмористических картинок, а затем - обыденной реальностью. Оранжевая книга превратилась в Common Criteria. Уровень A1/EAL7 остался все за тем же единственным лидером! Развивался интернет, появился и лопнул пузырь доткомов, худо-бедно какую-то сертификацию уже не в столь комической конфигурации, как поначалу, получил даже MS Windows. И вот, оказывается, в 2003 году Gemini Computers была приобретена компанией Aesec. Которая, наконец-то, позволила простым смертным ознакомиться с тем, как именно Gemini решили, казалось бы, принципиально неразрешимую задачу о невозможности обнаружения закладки в компиляторе. Как им удалось алгоритмически верифицировать компилятор?!
На сайте есть кучка презентаций, pdf'ок и в них - ответ на этот вопрос. И на многие другие. Как? Да очень просто. У них был компилятор, разработка которого проводилась, ну типа, под некоторым контролем. Вот его "приказом по лагерю" назначили доверенным. Ну и дальше можно тащить себя за волосы из болота.
-- Гоги, докажи что квадрат гипотэнузы равэн сумме квадратов катэтов?
-- Вах, учитэл, мамой клянус!
Вот примерно так. А специальное доверенное железо постороено на серийных x86 процессорах и других обычных китайских комплектующих. Да и собирается, небось, тоже в Китае.
Сама система построена хорошо, разумно, но ничем принципиально не отличается от обычных B-level систем или от российского "Феникса" (которого, впрочем, толком не бывает).
А чудес не существует.
Никто даже не мечтал проникнуть в Священные Тайны далее, ибо Коком.
Шли годы. Коком рассосался. url на двери общественного туалета стал сначала поводом для юмористических картинок, а затем - обыденной реальностью. Оранжевая книга превратилась в Common Criteria. Уровень A1/EAL7 остался все за тем же единственным лидером! Развивался интернет, появился и лопнул пузырь доткомов, худо-бедно какую-то сертификацию уже не в столь комической конфигурации, как поначалу, получил даже MS Windows. И вот, оказывается, в 2003 году Gemini Computers была приобретена компанией Aesec. Которая, наконец-то, позволила простым смертным ознакомиться с тем, как именно Gemini решили, казалось бы, принципиально неразрешимую задачу о невозможности обнаружения закладки в компиляторе. Как им удалось алгоритмически верифицировать компилятор?!
На сайте есть кучка презентаций, pdf'ок и в них - ответ на этот вопрос. И на многие другие. Как? Да очень просто. У них был компилятор, разработка которого проводилась, ну типа, под некоторым контролем. Вот его "приказом по лагерю" назначили доверенным. Ну и дальше можно тащить себя за волосы из болота.
-- Гоги, докажи что квадрат гипотэнузы равэн сумме квадратов катэтов?
-- Вах, учитэл, мамой клянус!
Вот примерно так. А специальное доверенное железо постороено на серийных x86 процессорах и других обычных китайских комплектующих. Да и собирается, небось, тоже в Китае.
Сама система построена хорошо, разумно, но ничем принципиально не отличается от обычных B-level систем или от российского "Феникса" (которого, впрочем, толком не бывает).
А чудес не существует.