John Rushby
Plus d'infos
- Connu pour
- Le noyau de séparation, PVS
- Affiliation
- SRI International
Informaticien britannique qui proposa en 1981 le noyau de séparation – l'idée que la façon la plus sûre de partager un ordinateur est de lui faire croire qu'il en est plusieurs.
Son article de SOSP 1981, « Design and Verification of Secure Systems », retourne le problème. Plutôt que de vérifier un système d'exploitation entier, un petit noyau ne fait rien d'autre qu'isoler des partitions les unes des autres : chacune se comporte comme une machine autonome, avec des canaux explicitement autorisés entre elles. Ce qu'il reste à prouver devient assez petit pour être réellement prouvé.
L'idée survit dans l'architecture MILS, dans l'avionique, les hyperviseurs et les micronoyaux modernes. À SRI International, Rushby a contribué à l'assistant de preuve PVS (1992), utilisé depuis pour vérifier aussi bien des algorithmes de commandes de vol que des protocoles cryptographiques.