Джон Раши
Британский учёный, в 1981 году предложивший ядро разделения: самый безопасный способ делить компьютер — заставить его притворяться несколькими.
Его статья «Design and Verification of Secure Systems» на SOSP 1981 года перевернула задачу. Вместо верификации всей операционной системы маленькое ядро занимается только изоляцией разделов друг от друга, так что каждый ведёт себя как отдельная машина с явно разрешёнными каналами между ними. Остаётся доказать так мало, что это можно сделать на практике.
Идея живёт в архитектуре MILS, в авионике, в современных гипервизорах и микроядрах. В SRI International Раши помогал создавать систему доказательств PVS (1992), которой с тех пор проверяют всё — от алгоритмов управления полётом до криптографических протоколов.