https://blog.invisiblethings.org/2010/05/03/on-formally-verified-microkernels-and.html
> One such thing is the correctness of a compiler, so that you can be sure that all the properties you proved for the source code, still hold true for the binary generated from this source code. Вот я ровно про это: сейчас Firefox предполагает корректность wasm2c, в то время как предпочтительнее было бы её формально доказать. Что сильно проще, чем доказывать корректность микроядра. Благо, у Wasm уже есть формальная спецификация.
Я нуб в васме, но вроде там линейная память в одном буфере. А потом это буфер оказывается опять в основной памяти приложения.
Во-первых, Wasm гарантирует корректную работу со стеком, и вообще не даёт делать со стеком что попало — это одно устраняет огромное количество дыр в безопасности. Во-вторых, даже в рамках одного процесса можно выделять память в отдельном сегменте так, что кусок кода оттуда никуда вылезти не сможет.
Хм, а можно про стэк подробнее? То есть вылезти из него да, нельзя, но внутри кода на васме без защиты стэка может происходить фигня
Обсуждают сегодня