3 ms·
It's only Monday and that paper lead me to L3 and the UNSW course[1] notes. There goes my next weekend or four. Thanks, ya son of a gun ;) [1] https://www.cse.
by iheartmemcache 10y ago
It's only Monday and that paper lead me to L3 and the UNSW course[1] notes. There goes my next weekend or four. Thanks, ya son of a gun ;)
[1] https://www.cse.unsw.edu.au/~cs4161/lect.html https://www.cse.unsw.edu.au/~cs4161/lect.html
- nickpsecurity 10y agoGlad you found something fun. If it's L3 for CPU's you mean, then one project of value nobody has done is put in specs for VAMP processor. It was mathematically verified in PVS as part of Verisoft project. They did OS and C subset for it. Adding it to L3 and Myreen et al's toolkit for doing machine code in Isabelle/HOL would let their spec-to-machine-code verifications run on a verified processor. Just throwing that out there for you or anyone interested in lengthening the chain of verification. VAMP doesn't get enough attention. On HW side, someone could do a verified front-end for RISC-V on top of the VAMP components to get a mostly-verified RISC-V. Lots of low-hanging fruit out there.