wizzard

Какие вы знаете безопасные (в смысле статически верифицируемые) виртуальные машины или форматы байткода?

(Также известно как typed assembly, proof-carrying assembler, managed code и такое прочее). Слайды по теме: http://www.cs.umd.edu/class/fall2006/cmsc631/lectures/talpcc.pdf

Я знаю BEAM (проконсультировался, увы, нет) и CLR.
JVM не подходит, потому что существующие формальные модели (http://cseweb.ucsd.edu/~gmporter/papers/formaljvm-ecoop01.pdf) не моделируют permissions, а смотрят только за integrity самого рантайма.

Требования примерно такие:

Level 0 protection: прога доказанно не может развалять рантайм (с этим проще всего, любой гипервизор или ОС на процессоре с MMU и ring levels подходит), на OOM, slowloris и прочее пока забьем для упрощения.

Level 1: прога доказанно не может развалять соседнюю прогу, иначе как через API (браузеры, JVM, dalvik, nacl, linux/bsd/windows/android итд итп)

Level 2: есть прога, из trusted library + untrusted code, антрастед код может звать методы из трастед либрари без оверхеда на IPC но доказанно не может обойти проверки, встроенные в них, даже если трастед лайбрари делает колбэки в untrusted код (CLR)

Level 3: в общем случае, можно навесить constraints на код, в виде security capabilities, и статически показать, что этот код будет доказанно их придерживаться (F*?)

репост с привлечением комментов в оригинал приветствуется. и, да, стоит ли на английском это написать? на stackoverflow такие вопросы не любят, увы.