Педагогическое

[audiart]

Хе-хе, proof-carrying code порвал аудиторию :) Я, в принципе, так и думала, меня он в свое время тоже порвал :)

Comments

[george-schwarm.livejournal.com]

proof-carrying code - что это?

[audiart.livejournal.com]

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

[dimabest.livejournal.com]

Звучит захватывающе. Хотя не представляю, как такое можно реализовать. Доказательство правильности алгоритма --- это да.

[audiart.livejournal.com]

Ой, в этой области столько рисерча делается в разных направлениях! Только это в основном не доказательство правильности алгоритма, а доказательство того, что программа багов не содержит, особенно security-critical.

[dimabest.livejournal.com]

Что я себе могу представить: написал я прогу, которая по каким-то критериям оценивает степень надёжности и безглючности кода. Результат работы программы будет указывать на степень надёжности, а подделать его не получится, ибо с помощью программы эту самую степень всегда можно ещё раз проверить.
Похоже?

[audiart.livejournal.com]

Не совсем. Такие программы есть, но проблема с ними в том, что процесс проверки обычно очень сложно. Поэтому идея такая: программа проверяет надежность кода и вставляет в него аннотации. Причем аннотации эти составляются таким образом, что с одной стороны с их помощью надежность программы гораздо проще проверить, а с другой - они настолько тесно зависят от кода программы, что если их изменить, не меняя код, это сразу будет заметно. Простейший пример - это проверка того, что когда программа выполняет jmp r1, она переходит к правильному адресу в кодовом сегменте. Если ты по "сырому" коду программы попытаешься выяснить, что к моменту прыжка хранится в регистре r1, это будет сложновато. А вот если перед каждой инструкцией стоит аннотация, в которой указано, что сейчас хранится в каждом регистре: просто число или валидный адрес, то все получается гораздо проще. И проверить, что аннотации соответствуют действительности, тоже легко: смотришь на аннотации до и после каждой инструкции, и сразу очевидно, правду тебе сказали или нет :)