3 ms·

The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pr

by throwway120385 2y ago

The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. And they really mean _reliability_ as in reliably wrong or reliably right. So being able to adjust the spec and fix the system is actually a feature because it means your prover acts as a high-quality test. As always, with systems like this if you use a formally-proven operating system kernel you will probably assess which other code paths in your application code are on the critical path and use formal methods on those components. And you will also be doing other less formal work like FMEA to complement. So you're not reliant on any one single method of assessing whether the system works, whether it meets the specification, and whether it can be relied upon to do the right thing in a bad situation.

ryao 2y ago
The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. The other guy mentioned phones, which run UNIX clones. It is fairly obvious that we were talking about computing in general, which includes all of the things you claim to be out of scope. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. Most embedded systems (e.g. the RP2040, the MSP430, etcetera) do not even have virtual memory protection, which makes seL4 a non option for them. When seL4 is an option, it is a tiny fraction of the code needed for the machine. All of that other code matters, especially since it is where the attack surface area is. seL4 on such machines is like the admin account in this picture; compromising what actually matters does not require compromising seL4: https://xkcd.com/1200/ https://xkcd.com/1200/ While seL4 is good at what it does, what seL4 does is extremely minimal and it is increasingly obvious that a vocal minority overrates it. Using seL4 is not going to stop vulnerabilities in userspace or even in drivers that were previously in kernel space, or in VMs running on top of it, but people who claim systems are insecure without seL4 insinuate that it will. They are like the Apple Store employee who once suggested to me that if I run Windows on Apple hardware, it will have none of the problems Windows normally has.

The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. And they really mean _reliability_ as in reliably wrong or reliably right. So being able to adjust the spec and fix the system is actually a feature because it means your prover acts as a high-quality test. As always, with systems like this if you use a formally-proven operating system kernel you will probably assess which other code paths in your application code are on the critical path and use formal methods on those components. And you will also be doing other less formal work like FMEA to complement. So you're not reliant on any one single method of assessing whether the system works, whether it meets the specification, and whether it can be relied upon to do the right thing in a bad situation.

ryao 2y ago

The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. The other guy mentioned phones, which run UNIX clones. It is fairly obvious that we were talking about computing in general, which includes all of the things you claim to be out of scope. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. Most embedded systems (e.g. the RP2040, the MSP430, etcetera) do not even have virtual memory protection, which makes seL4 a non option for them. When seL4 is an option, it is a tiny fraction of the code needed for the machine. All of that other code matters, especially since it is where the attack surface area is. seL4 on such machines is like the admin account in this picture; compromising what actually matters does not require compromising seL4: https://xkcd.com/1200/ https://xkcd.com/1200/ While seL4 is good at what it does, what seL4 does is extremely minimal and it is increasingly obvious that a vocal minority overrates it. Using seL4 is not going to stop vulnerabilities in userspace or even in drivers that were previously in kernel space, or in VMs running on top of it, but people who claim systems are insecure without seL4 insinuate that it will. They are like the Apple Store employee who once suggested to me that if I run Windows on Apple hardware, it will have none of the problems Windows normally has.