4 ms·

What about SEL4?

kaba0 5y ago
Written over many many years by experts of a field, and the end result is at most somewhat complex, nowhere near the complexity of even the monolith SPA of your favorite website.
- dnautics 5y ago
  GP said: > meaningful complexity Not, "the most complex". If an OS that can lock down DARPA self-flying helicopter software is not meaningful enough for you....
  - kaba0 5y ago
    Less than 10 000 lines of code. But let’s say we accept it as an exception — it is most definitely not the “standard way” of writing C programs.
    - dnautics 5y ago
      From GP: > It is not possible to remove ub from the spec did not say "it is not standard to remove ub"...
posix_me_less 5y ago
The speed of development was very low, and how many people can check the proofs?
- dnautics 5y ago
  > The speed of development was very low, Not a part of GP's assertion > and how many people can check the proofs? it's not necessary, the proofs are checked using automation. I'm directly taking a shot at this assertion: > Static analysis tooling has demonstrated that it isn’t up to the task
  - oscardssmith 5y ago
    Just because you have a proof doesn't mean it proves the right thing.
    - dnautics 5y ago
      Congratulations. You have won the argument "there is no perfectly secure system", which no one was arguing.
UncleMeat 5y ago
I've got a strong background in formal verification. I do not believe that "formally verified" means "security bug free". In fact, I personally know researchers who have had vulns found in their formally verified code more than a decade after they completed the verification.
- dnautics 5y ago
  I don't think there is any reasonable standard of security that demands perfection.
- posix_me_less 5y ago
  I agree, there are lots of outrageous claims out there about "provably secure software" which seem very dubious. What are your thoughts on SEL4, is it really a breakthrough it is made to be in success of formal verification? Is there a way for users/administrators deploying it to verify themselves authors' claims? Or is it too difficult? I am afraid the latter... In 2004 Peter Gutmann in his thesis/book criticized the hype around effectivity of formal methods in computer security [1]. Has the situation changed? [1] https://archive.org/details/springer_10.1007-b97264 https://archive.org/details/springer_10.1007-b97264
  - UncleMeat 5y ago
    Breakthrough? No. Good work? Yes.

What about SEL4?

Written over many many years by experts of a field, and the end result is at most somewhat complex, nowhere near the complexity of even the monolith SPA of your favorite website.

dnautics 5y ago
GP said: > meaningful complexity Not, "the most complex". If an OS that can lock down DARPA self-flying helicopter software is not meaningful enough for you....
- kaba0 5y ago
  Less than 10 000 lines of code. But let’s say we accept it as an exception — it is most definitely not the “standard way” of writing C programs.
  - dnautics 5y ago
    From GP: > It is not possible to remove ub from the spec did not say "it is not standard to remove ub"...

posix_me_less 5y ago

The speed of development was very low, and how many people can check the proofs?

dnautics 5y ago
> The speed of development was very low, Not a part of GP's assertion > and how many people can check the proofs? it's not necessary, the proofs are checked using automation. I'm directly taking a shot at this assertion: > Static analysis tooling has demonstrated that it isn’t up to the task
- oscardssmith 5y ago
  Just because you have a proof doesn't mean it proves the right thing.
  - dnautics 5y ago
    Congratulations. You have won the argument "there is no perfectly secure system", which no one was arguing.

UncleMeat 5y ago

I've got a strong background in formal verification. I do not believe that "formally verified" means "security bug free". In fact, I personally know researchers who have had vulns found in their formally verified code more than a decade after they completed the verification.

dnautics 5y ago
I don't think there is any reasonable standard of security that demands perfection.
posix_me_less 5y ago
I agree, there are lots of outrageous claims out there about "provably secure software" which seem very dubious. What are your thoughts on SEL4, is it really a breakthrough it is made to be in success of formal verification? Is there a way for users/administrators deploying it to verify themselves authors' claims? Or is it too difficult? I am afraid the latter... In 2004 Peter Gutmann in his thesis/book criticized the hype around effectivity of formal methods in computer security [1]. Has the situation changed? [1] https://archive.org/details/springer_10.1007-b97264 https://archive.org/details/springer_10.1007-b97264
- UncleMeat 5y ago
  Breakthrough? No. Good work? Yes.