poVoq@slrpnk.net to Permacomputing@slrpnk.netEnglish · 2 years agoThe ever-growing problem of ever-growing codebaseswww.theregister.comexternal-linkmessage-square2linkfedilinkarrow-up11arrow-down10
arrow-up11arrow-down1external-linkThe ever-growing problem of ever-growing codebaseswww.theregister.compoVoq@slrpnk.net to Permacomputing@slrpnk.netEnglish · 2 years agomessage-square2linkfedilink
minus-squaredemesisx@infosec.publinkfedilinkEnglisharrow-up1·edit-22 years agoI should make you aware of the fact that hardened, top-to-bottom formally verified OS’s exist. Some even go so far as to harden and formally verify both software and hardware. https://www.cs.ox.ac.uk/tom.melham/pub/Gao-2021-EFV.pdf https://github.com/standardsemiconductor/lion http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf https://www.cs.cornell.edu/courses/cs6410/2013fa/slides/10-verifiable-systems.pdf https://aerospacelab.onera.fr/sites/w3.onera.fr.aerospacelab/files/AL04-10_0.pdf https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD12/005.pdf
I should make you aware of the fact that hardened, top-to-bottom formally verified OS’s exist. Some even go so far as to harden and formally verify both software and hardware.
https://www.cs.ox.ac.uk/tom.melham/pub/Gao-2021-EFV.pdf
https://github.com/standardsemiconductor/lion
http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf
https://www.cs.cornell.edu/courses/cs6410/2013fa/slides/10-verifiable-systems.pdf
https://aerospacelab.onera.fr/sites/w3.onera.fr.aerospacelab/files/AL04-10_0.pdf
https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD12/005.pdf