SeL4 is old news - not a criticism, but has anyone added another formally proven layer or component? (Edit: I mean new components beyond the microkernel, not improvements to the microkernel.)
Also, I suspect some people - maybe some on HN :) - get emotional overload when they see the word 'proof' and their intellectual functions stop. It's not a panacea for the infinite problem of secure IT; it isn't a way to create or discover a perfect and flawless diamond of software. IIUC it means it's proven to meet specific requirements in specific conditions, and those requirements and conditions can be quite narrow; and it says nothing about other functions and conditions that are out of spec. Is that roughly correct?
What does it mean in practical terms? What does a security professional see when they see 'formally proven software'?
What are the specs that SeL4 meet (no, I haven't looked at the OP in a long time)? Isn't that the essential information here?
Also, I suspect some people - maybe some on HN :) - get emotional overload when they see the word 'proof' and their intellectual functions stop. It's not a panacea for the infinite problem of secure IT; it isn't a way to create or discover a perfect and flawless diamond of software. IIUC it means it's proven to meet specific requirements in specific conditions, and those requirements and conditions can be quite narrow; and it says nothing about other functions and conditions that are out of spec. Is that roughly correct?
What does it mean in practical terms? What does a security professional see when they see 'formally proven software'?
What are the specs that SeL4 meet (no, I haven't looked at the OP in a long time)? Isn't that the essential information here?