Announcement

Collapse
No announcement yet.

"The World's Most Highly-Assured OS" Kernel Open-Sourced

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

  • "The World's Most Highly-Assured OS" Kernel Open-Sourced

    Phoronix: "The World's Most Highly-Assured OS" Kernel Open-Sourced

    The seL4 kernel that's an advanced, security-enhanced version of the L4 micro-kernel has been open-sourced by General Dynamics C4 Systems and NICTA...

    http://www.phoronix.com/vr.php?view=MTc1MTg

  • #2
    Evil Corporate America®©™ strikes again.

    Comment


    • #3
      The Matrix now includes support for running SkyNet.

      Comment


      • #4
        What's it been assured of? Besides, a kernel is not an OS.

        Comment


        • #5
          I would be interested to know how many lines of code make up this kernel versus the Linux kernel.

          (I'm aware you can get this information fairly easily through Git, but I don't know how and I'm at work so haven't got time to research).

          Comment


          • #6
            Originally posted by kaprikawn View Post
            I would be interested to know how many lines of code make up this kernel versus the Linux kernel.

            (I'm aware you can get this information fairly easily through Git, but I don't know how and I'm at work so haven't got time to research).
            I didn't count the lines but tar.xz of Linux 3.15.7 is 79.7MB while zip of master branch for seL4 is 953.4kB

            Comment


            • #7
              Originally posted by Cyborg16 View Post
              What's it been assured of? Besides, a kernel is not an OS.
              Seem more like an abstraction layer between hardware and Linux rather than independent kernel.

              Comment


              • #8
                Originally posted by kaprikawn View Post
                I would be interested to know how many lines of code make up this kernel versus the Linux kernel.

                (I'm aware you can get this information fairly easily through Git, but I don't know how and I'm at work so haven't got time to research).
                About 7500 lines of code.

                Comment


                • #9
                  Originally posted by Pawlerson View Post
                  Seem more like an abstraction layer between hardware and Linux rather than independent kernel.
                  Linux can be run in a vmm above this kernel but it is an independent (micro)kernel in itself.

                  Comment


                  • #10
                    Originally posted by jayrulez View Post
                    About 7500 lines of code.
                    Thanks, wow that's quite something. A quick google search shows the Linux kernel was over 15million lines of code in 2011. I suppose it's a lot easier to keep code secure when there's so few moving parts.

                    For limited use cases I'm sure this would be good to use. Though with so few lines of code I'm assuming there's no hardware drivers. Imagine getting wi-fi up-and-running using this!

                    Comment


                    • #11
                      Originally posted by kaprikawn View Post
                      I would be interested to know how many lines of code make up this kernel versus the Linux kernel.

                      (I'm aware you can get this information fairly easily through Git, but I don't know how and I'm at work so haven't got time to research).


                      I don't think the aim the same hardware coverage. Drivers alone are a huge part of linux kernel.

                      Comment


                      • #12
                        Originally posted by kaprikawn View Post
                        Thanks, wow that's quite something. A quick google search shows the Linux kernel was over 15million lines of code in 2011. I suppose it's a lot easier to keep code secure when there's so few moving parts.

                        For limited use cases I'm sure this would be good to use. Though with so few lines of code I'm assuming there's no hardware drivers. Imagine getting wi-fi up-and-running using this!
                        There are a few drivers available for various platforms. The drivers are run in userspace so so they do not add to the complexity of the kernel. With the right layers above, it could be used for the same scenarios that Linux is used for. Of course, platform, libraries and driver support aren't even near the same level that Linux is.

                        Comment


                        • #13
                          Originally posted by by.peroux View Post
                          I don't think the aim the same hardware coverage. Drivers alone are a huge part of linux kernel.
                          Yeah, microkernels as this one will usually be running drivers in user space anyway.

                          Comment


                          • #14
                            You can always use DDEKit with linux drivers on an L4 kernel; probably not without possible bugs, but if you're doing something like that you would probably have time to check for bugs yourself.

                            Comment


                            • #15
                              Originally posted by Nobu View Post
                              You can always use DDEKit with linux drivers on an L4 kernel; probably not without possible bugs, but if you're doing something like that you would probably have time to check for bugs yourself.
                              It's not a given that DDEKit works for any L4 kernel. seL4 currently does not use/support DDEKit. DDEKit is used with older and newer versions of Fiasco, Minix, Hurd and Genode. Note that DDEKit is different for each of these OS/Kernels.

                              Comment

                              Working...
                              X