Announcement

Collapse
No announcement yet.

seL4 Micro-Kernel Working Towards A General-Purpose, Multi-Server OS

Collapse
X
 
  • Filter
  • Time
  • Show
Clear All
new posts

  • #31
    Originally posted by Nemerian View Post
    Wasn't Genode OS used with L4?
    Yes https://genode.org/documentation/articles/sel4_part_2

    Genode has a bunch of kernels under his belt https://genode.org/documentation/platforms/index

    Comment


    • #32
      Originally posted by pabloski View Post
      Looking around, I couln't find if SculptOS (their precompiled binary) was using SeL4 by default under the hood.

      If so, I'm definitely trying it! It looks so cool.

      Comment


      • #33
        Originally posted by Rallos Zek View Post
        That's just the kernel part that has been verified, none of the drivers and glue code which would make it work has had the same testing or verification applied to them.
        btw :
        Formal verification (alias proof of correctness) has been found to be as error-prone as software construction itself, and for that and other reasons it is unlikely to be that silver bullet (Glass 2002).
        Last edited by pal666; 07 February 2021, 12:39 PM.

        Comment


        • #34
          Originally posted by microcode View Post

          No, this is not TDD; this is an actual system of mathematical and symbolic proofs. It is a completely different galaxy of verification.

          Something that you get with proofs that you do not get with tests, is a complete picture of what the code could do (assuming the processor is functioning as designed, and your model of it is accurate), not just the subset of what it should/might do that you think of when you're writing tests.


          Congratulations on being scooped up by marketing. No It's literally just as I said. Oh boy you have 100% code coverage on your tests which means you were following TDD. "Mathematically Proven" is as much a bullshit term as "Artificial Intelligence". It is only suitable for annoying actual developers.

          Comment


          • #35
            Originally posted by pal666 View Post
            Formal verification (alias proof of correctness) has been found to be as error-prone as software construction itself, and for that and other reasons it is unlikely to be that silver bullet (Glass 2002).
            Come to think of it... when was the last time there was actually a significant Linux kernel exploit rather than a hardware exploit or a userspace exploit?

            Comment


            • #36
              Originally posted by Luke_Wolf View Post

              Come to think of it... when was the last time there was actually a significant Linux kernel exploit rather than a hardware exploit or a userspace exploit?
              Bleeding tooth?

              I love what Linux stands for (user freedom / open source), but I would gladly accept a smaller & more secure kernel if there weren't too many compromises.

              Comment


              • #37
                Originally posted by kvuj View Post

                Bleeding tooth?

                I love what Linux stands for (user freedom / open source), but I would gladly accept a smaller & more secure kernel if there weren't too many compromises.
                I guess? But that's a driver bug that seL4 having complete test coverage wouldn't have protected against either. Microkernel architecture in general could potentially stop the privilege escalation (you actually need certain hardware guarantees around memory access) but it wouldn't stop the underlying security flaw.

                Comment


                • #38
                  Originally posted by Luke_Wolf View Post

                  I guess? But that's a driver bug that seL4 having complete test coverage wouldn't have protected against either. Microkernel architecture in general could potentially stop the privilege escalation (you actually need certain hardware guarantees around memory access) but it wouldn't stop the underlying security flaw.
                  Yes it would. It's not a security flaw if all you have is a crashed driver. duh.

                  Comment


                  • #39
                    Originally posted by bofh80 View Post

                    Yes it would. It's not a security flaw if all you have is a crashed driver. duh.
                    Ah yes because it's not as if a Network Protocol Stack contains information that would potentially be bad to have leaked or anything, which is what Bleeding Tooth is as much about.

                    Comment


                    • #40
                      Originally posted by Rallos Zek View Post

                      That's just the kernel part that has been verified, none of the drivers and glue code which would make it work has had the same testing or verification applied to them.
                      Geez, a bunch of people here seem to think that software reliability is all or nothing, and that having a reliable kernel is useless.

                      Comment

                      Working...
                      X