The Holy Grail of Static Verification and Static Typing

[wizzard]

There is no such thing.

It’s a trade-off. Even in computers, there is no such thing as perfectly reliable code, there’s only how much resources you’re willing to pay for the next improvements. It’s easy to be oblivious to this. I can’t even count the number of times said some variation of “OK, now I know it works” before I learned that it will always break. Always.

Failure is inevitable. If you want to build anything large and to last, you have to incorporate it into your design and build organic systems that monitor, recover, repair, and, above all, fail gracefully when they themselves inevitably fail.

Holy Grail этот самый, короче, достижим только в случае неизменного окружения, неизменного ТЗ и исключения человеческого фактора. Чего в природе не бывает.

Comments

[gds.livejournal.com]

ну нет же, есть perfectly reliable code, например, полученный экстракцией из доказательства.
А типизация -- это минимальные гарантии. Если типизация не вызывает проблем, то лучше иметь эти гарантии, чем не иметь.
Она позволяет легко делать простой рефакторинг ещё, например, тогда как в случае динамической типизации это нереально (там транслятор не знает о типах, поэтому не может помочь при изменении типа данных; я часто делаю рефакторинг, меняя типы, и ничего не ломается по определению).
Ещё одно клёвое свойство статической типизации состоит в том, что ей покрыт весь код, тогда как в случае динамической типизации необходимо принимать меры к тому, чтобы тестирование/рефакторинг покрывало весь код.

[wizzard]

Я бы сказал, что полезно иметь возможность их комбинировать
и\или infer'ить типы, и\или, как это сейчас модно говорить, делать gradual typing (в смысле, когда код типизируется в процессе стабилизации интерфейсов и пр.)

[gds.livejournal.com]

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

[xplozive.livejournal.com]

В XCode, кстати, недавно добавили инструмент для статического анализа Objective-C кода. Довольно умная штука, реально дохуя багов в production-коде нашло. Насколько помню, базируется на каком-то доказателе теорем.

[wizzard]

В VS есть Code Contracts со статик чекером. Тоже доказатель теорем, да :)

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

[vkorenev.livejournal.com]

Инженерные конструкции можно рассчитывать на прочность, а можно строить на глазок. Динамическая типизация, ИМХО, аналог строительства на глазок: быстро и очень даже уместно, когда надо сарай построить. А авиалайнеры хорошо бы всё-таки рассчитывать на прочность.

[wizzard]

Да. Но даже в рассчитанном авиалайнере встраиваются резервные системы, that's the point of this post.

[antonix.livejournal.com]

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

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

[vkorenev.livejournal.com]

Пойнт статьи в том, что сколько не резервируй, а катапультируемое сидение лучше поставить, да и завещание написать.

[109.livejournal.com]

http://push.cx/2008/now-do-you-know-it-works ?

[wizzard]

О! Спасибо)

А то я это из драфта поста откопал, полугодовалой давности)

[aka-rider.livejournal.com]

Эм. Ну что сказать? Мой софт работает, просто работает. Но согласно SLA, а я в своей жизни не видел SLA на 100% availability.
И если это софт кардиостимулятора, чем плох static verification, который гарантированно повысит надежность кода?
Лично я за виртуализацию и sandboxing, и я против JIT. Благо по вычислительной мощности у программистов большой запас, просто сейчас она утилизируется восновном на RAD.

[wizzard]

Static verification не плох. Плохо на него надеяться.

А почему против JIT, если не секрет? :)

[aka-rider.livejournal.com]

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

[wizzard]

Да, согласен.

Собственно, как и paravirtualization. Другой вопрос, что громоздить друг на друге чистые интерпретаторы как-то очень расточительно выглядит... (imagine OS->VM->OS->browser->browser JS, for example)

Security vs performance, хехе.

[aka-rider.livejournal.com]

>OS->VM->OS->browser->browser JS
А движемся как раз в эту сторону. Исходя из того, что все крупные абстракции текут, тот самый browser JS будет позволять выполнить native код на ring0 :)

[wizzard]

Я неоднократно BSOD'ил WinXP/Vista/7 SWF'ками, когда экспериментировал с их аппаратным ускорением :)

Дальше ковырять было лень...

[aka-rider.livejournal.com]

Это интересно, от 7-ки не ожидал, там же часть с аппаратным ускорением вынесена из ядра.
Кстати, неплохо было бы в MS те самые swf'ки заслать, у них приоритет багов от пользователей выше, чем от штатных тестировщиков. Так что больше шансов что поправят.

[wizzard]

nVIDIA drivers account for more than 30% of *all* BSODs :)

Т.е. там пофигу, любая железка, умеющая DMA - это такой аппаратный эксплоит, если дрова кривые. FireWire тот же, да)

[aka-rider.livejournal.com]

А, ну да.
Ну Семен писал, что раньше еще веселее было, пока DX инфраструктура в ядре крутилась. То есть компилятор шейдеров, как пример.

Хех, все никак времени нет minix3 расколупать (драйверы устройств в user-space) и почитать Татенбаума вдумчиво. А там глядишь - свой Болгенос напишу.

[aka-rider.livejournal.com]

Хотя, я все-таки не совсем правильно выразился. Я не против JIT в JVM/.NET (у них все-таки задачи другие), но меня сильно беспокоит его наличие скажем в браузере.

[wizzard]

Ну, собственно, та же хрень - даже если разрешить JIT только подписанному коду, все равно найдется глупая комбинация из http://www.epagini.com/2010/08/stuxnet-the-trojan-horse-with-realtek-digital-signature/ + http://www.microsoft.com/technet/security/bulletin/ms07-040.mspx :)

[wizzard]

Да, кстати, чистые интерпретаторы тоже бывают дырявыми - http://www.securiteam.com/securitynews/5VP0115S0G.html :))))))

[aka-rider.livejournal.com]

Это логично, сразу же вспомнил: На что был похож код в Imaging
Навскидку можно сказать, что интерпретаторы с JIT еще более дырявые :)))

[thedeemon.livejournal.com]

В Flash Player 9 и 10 уже давно JIT.

[wizzard]

>> An integer overflow exists in the AVM2 abcFile parser code which handles the intrf_count value of the instance_info structure.

Но уязвимость не в JIT.