Previous Entry Share Next Entry
2016-01

The Holy Grail of Static Verification and Static Typing

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 этот самый, короче, достижим только в случае неизменного окружения, неизменного ТЗ и исключения человеческого фактора. Чего в природе не бывает.


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

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

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

(Deleted comment)
wizzard0 August 10th, 2010
В VS есть Code Contracts со статик чекером. Тоже доказатель теорем, да :)

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

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

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

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

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

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

wizzard0 August 10th, 2010
О! Спасибо)

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

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

wizzard0 August 10th, 2010
Static verification не плох. Плохо на него надеяться.

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

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

wizzard0 August 10th, 2010
Да, согласен.

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

Security vs performance, хехе.

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

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

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

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

wizzard0 August 10th, 2010
nVIDIA drivers account for more than 30% of *all* BSODs :)

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

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

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

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

wizzard0 August 10th, 2010
Ну, собственно, та же хрень - даже если разрешить 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 :)

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

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

thedeemon August 11th, 2010
В Flash Player 9 и 10 уже давно JIT.

wizzard0 August 11th, 2010
>> An integer overflow exists in the AVM2 abcFile parser code which handles the intrf_count value of the instance_info structure.

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

  • 1
?

Log in

No account? Create an account