Lions OS: secure – fast – adaptable

(trustworthy.systems)

138 points | by snvzz 13 days ago

8 comments

  • tommiegannert 13 days ago
    Seems to be this:

    https://www.lionsos.org/

    https://github.com/au-ts/lionsos

    > LionsOS is aimed at embedded, IoT and cyberphysical systems and is designed to be formally verifiable, adaptable to a wide class of use cases in the target domain, while at the same time setting the benchmark for performance of microkernel-based operating systems. We aim to achieve all three goals by a highly modular yet ruthlessly performance-oriented design and strict adherence to the time-honoured KISS principle.

    • alex_suzuki 13 days ago
      What, pray tell, are “cyberphysical” systems?
      • saithound 12 days ago
        It is a term coined by the Air Force Research Laboratory, as an umbrella term for industrial control systems, robotics, avionics, and generally any system that primarily consists of software and the heavy machinery it operates.

        The term is favored by DARPA over any of its alternatives; seL4 received DARPA funding, and was adopted by DARPA projects, so it's not surprising that they'd use the associated term. It's no worse than other terms in the embedded systems world, and communicates the intended use cases to the most likely users.

        Basically, if TrendMicro builds you a bunch of infrastructure to optimize the power grid, it will be described as consisting of Intelligent Electronic Devices. If Collins Aerospace builds the exact same infrastructure, it will be described as consisting of Cyber Physical Systems.

      • subjectsigma 13 days ago
        https://www.google.com/search?q=cyber+physical+systems

        Factory equipment, vehicles, drones, power grids, medical robots, HVAC, … the list goes on.

        • foundry27 12 days ago
          Also involved with some of these industries, no academia/government though, so my perspective may be incomplete. Anecdotally I can’t remember hearing this term used.

          After reading the Wikipedia page and a couple corporate pages about cyberphysical, I think it looks like it’s more about rebranding existing systems that contain interacting heterogenous elements with different RT needs, rather than introducing fundamentally new systems methodologies or technologies. It kinda reminds me of Agile, where a shift in mindset and terminology was hyped way more than any legitimate improvement in the underlying systems being built, and engineering “Agile products” became so important for some businesses.

        • 0xEF 13 days ago
          I work in the industry that builds and integrates most of that stuff. We don't use that term. It's marketing woo which is why the other commenter has probably never heard it.
          • subjectsigma 12 days ago
            I work in defense and it is extremely common. That doesn’t mean it isn’t marketing fluff, but I was genuinely surprised they didn’t know and/or thought they were being snarky.
          • Luc 13 days ago
            > It's marketing woo

            Nah, it's a term used in academia.

            • feldrim 12 days ago
              IIRC it started with government institutions and think tanks, and quickly adopted by academia.
              • monocasa 12 days ago
                Yeah, you pick up .gov buzzwords pretty quickly if you want your grants approved.
            • arghwhat 12 days ago
              Feels like a term used in academia unrelated to the actual field itself...
  • defrost 12 days ago
    Tangentially related

    https://en.wikipedia.org/wiki/A_Commentary_on_the_UNIX_Opera...

    The LionsOS name is a direct callback to the John Lions Lions' Commentary on UNIX 6th Edition, an Australian computer scientist and somewhat nomadic Professor.

    Trustworthy, as seen in the post link, also hails from New South Wales.

    • pjmlp 12 days ago
      One of the reasons UNIX won over the other proprietary systems, without the book and the related AT&T drama, most universities wouldn't have bothered.
  • 1oooqooq 13 days ago
    hope this message gets reminded in 10yrs as the email Linus announcing his toy kernel.
  • pgraf 13 days ago
    Can anyone elaborate which (proposed) advantages LionsOS has over Genode?
    • onjectic 12 days ago
      Just as new to LionsOS as you are, but it has a much more permissive license, and it’s not dual licensed. I think this will make it easier for people to support the project.
    • vilvo 12 days ago
      Correctness via formal verification - at least in the core of sel4.
      • monocasa 12 days ago
        Genode can also run on sel4.
        • nickpsecurity 12 days ago
          Are its TCB and integration similarly verified? If not formally-verified, are they in a safe language or statically analyzed to block common errors?
          • monocasa 12 days ago
            I mean, LionOS appears to (with the exception of sel4 itself) be mainly written in unverified C without heavy static analysis.

            So LionOS and Genode appear to be about equal in that regard.

  • jmakov 13 days ago
    Where's the talk. On their web site there are only slides.
    • microkerneldude 13 days ago
      the talk link will appear as soon as Everything Open uploads it
  • knighthack 13 days ago
    Question: under what circumstances would I ever want to use this OS, over Linux or MacOS or Windows?
    • mikewarot 13 days ago
      I've been waiting for a system like this for over a decade to use as my daily driver. An OS that runs with a capability model like this is immune to whole classes of security exploits that guarantee Linux, Windows, MacOS, etc. will never be secure.

      I was hoping Genode would get there sooner, and GNU Hurd should have gotten there years ago.

      Capabilities are the computing version of circuit breakers. They make it possible to run code without having to trust it. You can't do that with Linux, Windows, MacOS, et al. MULTICS could do it, but it was deemed too complex, at the time.

      • amluto 12 days ago
        FWIW, I would not trust seL4 on x86. Last time I checked, seL4’s interaction with the x86 architecture was not formally verified and looked quite buggy.

        Even a microkernel has three things that form part of the TCB: the part that interfaces with the even-lower-level stuff (interrupt and exception handlers, paging, memory model, etc), the interface it provides to its clients (syscalls and whatever it provides via syscalls), and the code that glues the first two parts together and implements the microkernel’s internal logic.

        The latter two, in seL4, are straightforward and formally verified. The former, on x86, not so much.

        AIUI, the situation on ARM is likely better.

        • snvzz 12 days ago
          >FWIW, I would not trust seL4 on x86.

          I would not trust any system on x86.

          >AIUI, the situation on ARM is likely better.

          Somewhat, but still not good.

          RISC-V is where it's at, when it comes to seL4.

          (seL4 participates in RISC-V)

      • sillywalk 12 days ago
        Have you tried Genode's Sculpt OS?

        "Sculpt is an open-source general-purpose OS. It combines Genode's microkernel architecture, capability-based security, sandboxed device drivers, and virtual machines in a novel operating system for commodity PC hardware and the PinePhone. Sculpt is used as day-to-day OS by the Genode developers."

        https://genode.org/download/sculpt

        • mikewarot 11 days ago
          I tried it a while ago, it seemed like there wasn't enough there, there. I couldn't find the "Hello World" example that made sense to me. I get the idea of composing resources, but until I've got a file system and compiler running, and a command line I can do something with, it doesn't help. 8(

          I'm hoping that Sculpt 24.04 does the job for me. If I can make sense of it enough to get Free Pascal running on it, or even just a C compiler, and "Hello, World" in a CLI, we're off to the races.

          • sillywalk 10 days ago
            I never really got it to do anything. I gather that this[0] is the "tutorial", and it looks complicated. Just allocating hardware etc.

            I suppose that's part of the price for high-security.

            I don't have an x86 machine, and running it under a VM is too slow.

            https://genode.org/documentation/articles/sculpt-22-04

      • progbits 13 days ago
        Do you know if there is anything like that which can run OCI containers/lightweight VMs? I would love that as daily driver too for the same reasons, but realistically will have to run various Linux apps to be productive, so those could go into shortlived isolated sandboxes ala distrobox.
    • subjectsigma 13 days ago
      Under no circumstances, it’s a microkernel for embedded systems.

      It’s like asking under what scenarios would you want to drive an ATV through New York. Technically possible, but that’s just not what it was made to do.

      • blacklion 13 days ago
        In practice, Linux is everywhere now, often in places where it should not be.

        Linux is truck/SUV of computer world if I can extend your analogy. It doesn't belong to center of big city, but it is here.

        • Affric 12 days ago
          My conversations with people who have implemented Linux where it shouldn’t have been have essentially boiled down to it being easier to hire Linux developers than embedded systems developers
          • blacklion 12 days ago
            Yes, it is "good enough" and familiar to everybody in industry. I understand that. But it doesn't mean we don't need to try harder.
          • ertian 12 days ago
            It's easier to hire linux kernel devs, there's more documentation, tooling & examples, device drivers & filesystems are more widely available, etc.

            Every other OS has to play catch-up. They either need a killer app or lots of funding, or else they'll be stuck in a specific niche.

    • devit 13 days ago
      All circumstances where correctness and security are more important than maximum possible performance, once it's mature enough (which will probably never happen), since it provides a proper and secure architecture.
      • RetroTechie 13 days ago
        Which is basically everywhere.

        Well-designed microkernels have been proven to have only a minor impact on performance, afaik. Especially if said kernel is small enough to fit in a cpu's L1 or L2 cache entirely.

        With that in mind, I'd say there's few cases left where users would not want to take a minor performance hit, if that gets rid of entire classes of bugs & vulnerabilities.

        Reasons this isn't the norm these days are mostly historic. But going forward, a good midpoint would be popular OS kernels like Linux split into smaller components, while providing same user-space APIs. Along the lines of how XFree86 was modularized into a set of Xorg libraries. Maybe L4Linux could be an example? (dunno how modular that is though).

        On such a componentized system, components could be shared among multiple 'OS personalities'. Kinda like a multi-VM setup but finer grained with much more shared code, much reduced attack surface for individual components, while maintaining very strong isolation guarantees between components.

      • snvzz 12 days ago
        seL4 is not doing badly in the performance side. It is even seen beating Linux in the slides.
  • mtmk 12 days ago
    When I saw 'Sydney 2052' for a split second I felt like I was in a sci-fi movie :D
  • superidiot1932 13 days ago
    Sorry for hijacking this thread but I've tried multiple times to post the announcement of Lions OS weeks ago and it always got shadow deleted:

    https://news.ycombinator.com/item?id=39920624

    https://news.ycombinator.com/item?id=39933112

    • Solvency 12 days ago
      this site is run and shadow manipulated by mods to bestow karma/credit points to a chosen few posters. you're not in the club.
      • jermaustin1 12 days ago
        I'm a nobody in every sense of the word. I didn't go to a fancy school; I didn't join a startup or a unicorn; I've worked as a corporate web dev for 20 years using ASP.Net and C#; I know very few people in tech (and no one high up).

        My posts are never "shadow deleted" they in fact sometimes get a boost from the mods when they though it just missed the mark timing-wise (i.e. interesting post, but some breaking news thing happened, and I didn't get the love).

        The moderators only car about keeping the discord civil (as civil as possible), and the posts relevant/interesting for their niche.

        There probably is a "club" - but not being in it doesn't get your content shadow deleted. It just wasn't interesting enough at the time to get votes.

        • Solvency 12 days ago
          I am not the original poster, so what's your explanation for why his two attempts were both deleted?
          • pvg 12 days ago
            They weren't deleted, the account was brand new when they were posted so they were probably killed by the spam detector. Questions about stuff like that should just be sent to hn@ycombinator.com, that's in all the site docs.
            • aprilnya 12 days ago
              A spam detector that just kills anything from people new to the site, + it not ever being reviewed/revived, is pretty uncool IMO.
              • pvg 12 days ago
                That would be a bad spam detector but it's obviously not one HN uses, not sure how you reached that conclusion.
                • aprilnya 12 days ago
                  That’s what I inferred from your comment
                  • pvg 12 days ago
                    Nothing like your inference was in my comment, beside the seemingly obvious fact nobody would use such a 'spam detector'. But either way, you can trivially verify this yourself just by looking at /newest.
                    • aprilnya 12 days ago
                      > the account was brand new when they were posted so they were probably killed by the spam detector
                      • pvg 12 days ago
                        Right, that's what I wrote. It doesn't say 'all posts by new users are killed without review'. Like, why would anyone do that? How would the site work?
              • jermaustin1 12 days ago
                They are speculating, but there is no telling if it ever even happened. I tend to believe the site's news was just more interesting than what OOP posted.
                • seti0Cha 12 days ago
                  That's Paul Graham's account, so maybe not just speculation. I didn't realize he still read this site. Not to jump on to OPs paranoia but I kind of thought he was frequenting some secret meta-HN site that still talks about entrepreneurship. Paul, if you see this, let me in! I swear I won't complain about capitalism!
                  • pvg 12 days ago
                    It's my account, not Paul Graham's.
                    • tptacek 11 days ago
                      Hmmm sounds like something Paul Graham would say.
                      • pvg 10 days ago
                        Makes me wonder if anyone has ever made up a sovereign citizen-style conspiracy theory except the person is a government agency. Like the man somehow just assigns a real person to be one rather than be employed by one, represent one, etc. There's some complicated legal reason for this and, of course, it gives you some sort of superpowers and/or freedom from consequence. Seagal-style movie trailer practically writes itself: Thomas Ptacek IS NSA.
                        • tptacek 10 days ago
                          I flagged this comment.
                    • seti0Cha 12 days ago
                      It appears my memory has failed me yet again. Sorry about that, pvg!
          • striking 12 days ago
            If I had to guess, their username contains "idiot" and so might have tripped up the spam detector.

            But you can always email the mods. They're very responsive.

          • santoshalper 12 days ago
            Who knows - maybe different mods have different criteria/bias? Maybe today is a slow day?

            I mean, this post isn't really big news, it feels like it's just barely scraping by the notability/interest level required to make it on HN. Mostly, I just think the presence of some kind of cabal or conspiracy is a lot less likely than "mods are human and thus subjective and inconsistent".