7 ms·
Integrity-178B: Safety Critical Real-Time OS
- Animats 3y agoGreen Hills Software? They're still around, and doing good things? That's impressive.
- f1shy 3y agoAround, yes. Doing good things… ehm well, they do things, not the best, and are arrogant as hell.
- KRAKRISMOTT 3y agoWeren't they the ones who sued tesla?
- mips_r4300i 3y agoVxWorks wants know your location...
- joezydeco 3y agoWhereas Green Hills wants to see your accounting books.
- jtwaleson 3y agoThe fight that their founder and CEO had with Elon on twitter was so weird. Came across as a complete crackpot saying his software is perfect and can never be hacked. That sounds insane but then actually having built the OS that meets these standards is impressive as hell. I’m still very confused about it.
- sillywalk 3y agothis? https://www.motortrend.com/features/tesla-full-self-driving-ban-attempt-elon-musk-dan-odowd/ https://www.motortrend.com/features/tesla-full-self-driving-...
- jtwaleson 3y agoIt’s a long running feud I believe. Look at his twitter profile and website to see how he communicates.
- seabird 3y agoYour takeaway from that was that the Green Hills CEO is a crackpot? Tesla's attitude toward automotive engineering and safety would be a funny joke if fucking these things up didn't get people killed. Tesla may be rigorous by Silicon Valley junkware standards, but they would be laughed out of the room in the places where Green Hills operates.
- jtwaleson 3y agoNo he came across as one. Look at his website and tell me you don’t think the way he presents himself is weird: https://danodowd.com/ https://danodowd.com/ I’ve met engineers with a similar attitude and they were the worst people to work with. But then again, his accomplishments are incredible. So: I’m confused.
- mighmi 3y agoDon't be confused. He just needs a better copywriter. Realize that in aerospace etc. this is possible where 9-12 9s of reliability are the common minimum accepted. Communicating this to a field which strives towards 5 9s and is used to charlatans is difficult, and he isn't succeeding. His chosen expressions sound bombastic and conversation ("can't be hacked") compared to the technical equivalents, but developers and engineers outside of this subfield wouldn't fully understand them. > I can make any program run much faster, often 4x does sound baffling but when backed up by his laurels, we can charitably imagine what he really means - and it's not so difficult either. From the bottom of the barrel, using slightly better algos in python to rewriting it in rust, we can all do this. His company presumably goes further with Ada, formal methods and exotic tooling to get extra performance out of microcontrolers.
- veqq 3y agoWhat do you mean by arrogant as hell? I'd not heard much about them.
- GnarfGnarf 3y agoHow much is a license for their OS?
- AlotOfReading 3y agoEnterprise pricing. Specific to each customer, but if you don't have a team of lawyers, you can't afford it. You'll need those lawyers to deal with the contract provisions limiting you from using open source software and argue about how many seats you're actually licensing.
- jnwatson 3y agoLast time I heard a few years ago, it cost low seven figures by the time you're done with everything. There's not a lot of competition in this space.
- inamberclad 3y agoHowever much you can pay. Millions. Not even joking. It may be worth it for a big ticket aircraft program though.
- johnea 3y agoIf you have a large gov contract for incinerating the poor, this is the OS for you...
- askiiart 3y agoI'm not gonna comment on the "incinerating the poor part", that's a whole debate I'm not getting into, but I can say for certain that this is what runs on the F-35. Source: my dad works on the F-35 program. Also there's a picture of the F-35(C) on their site, but I only thought to check after: https://www.ghs.com/AerospaceDefense.html https://www.ghs.com/AerospaceDefense.html
- thebruce87m 3y agoI always wonder if people making these kind of comments know of the risks. Is your dad happy about you giving this info away? Does it make you a target to get to him? Do the state actors have all of this info anyway? Are you fake and in fact a honeypot?
- gavinsyancey 3y agoThis is public info: https://www.ghs.com/customers/lockheedf35.html https://www.ghs.com/customers/lockheedf35.html
- serf 3y agothe F35 project created ~240,000 American jobs, many of which do not require any kind of special clearance or security measures. "My family worked on X" isn't at all alluring when we're talking about a huge public mass production of something. >Is your dad happy about you giving this info away? the F35 use of this software is public data.[0], and 'Dad's Happiness' isn't relevant to an internet stranger. >Do the state actors have all of this info anyway? State actors most definitely know these kind of details, they're likely not very actionable without lots of effort; that's why they're public. >Does it make you a target to get to him? It rarely matters who is a target, secretive projects are typically composited in such a way as to reduce the liability and overall management access of singular entities and individuals -- in other words 'Dad' isn't ever a lynch-pin for the entire operation. I don't know if he's fake, or a honey-pot; but it seems like a big waste of effort and resources if that's the case. source: aerospace family. [0]:https://www.ghs.com/customers/lockheedf35.html https://www.ghs.com/customers/lockheedf35.html
- Veserv 3y agoYou can see the SKPP certification requirements here: https://www.commoncriteriaportal.org/files/ppfiles/pp_skpp_hr_v1.03.pdf https://www.commoncriteriaportal.org/files/ppfiles/pp_skpp_h... You can see the Security Target specification and how it conforms here: https://www.commoncriteriaportal.org/files/epfiles/st_vid10362-st.pdf https://www.commoncriteriaportal.org/files/epfiles/st_vid103... You can see the certification report here: https://www.commoncriteriaportal.org/files/epfiles/st_vid10362-vr.pdf https://www.commoncriteriaportal.org/files/epfiles/st_vid103... Of note in the certification requirements are: "For example, SKPP separation mechanisms, when integrated within a high assurance security architecture, are appropriate to support critical security policies for the Department of Defense (DoD), Intelligence Community, the Department of Homeland Security, Federal Aviation Administration, and industrial sectors such as finance and manufacturing." AVA_VLA_EXP.4 Highly Resistant on page 116: "The NSA evaluator shall perform an independent vulnerability analysis." "The NSA evaluator shall perform independent penetration testing." "The NSA evaluator shall determine that the TOE is resistant to penetration attacks performed by an attacker possessing a high attack potential." First party NSA penetration test and analysis certifying it is appropriate for critical DoD systems. Note that the system is used on the F-35. ADV_FSP_EXP.4 Formal Functional Specification on page 92: "The developer shall provide a formal presentation of the functional specification of the TSF." Formal specification of the code. "The evaluator shall determine that the functional specification is an accurate and complete instantiation of the TOE security functional requirements." Formal specification matches the requirements. ADV_IMP_EXP.3 Structured Implementation of the TSF on page 93: "The developer shall make available, the implementation representation for the entire TSF." Full source code provided to evaluator. "The implementation representation shall unambiguously define the TSF to a level of detail such that the TSF can be generated without further design decisions." Source -> Binary translation is verified.
- jnwatson 3y agoIt is interesting to look at the SKPP and what a conforming implementation ensures against seL4, which has been formally verified to be correct. SKPP requires non-interference but not actual correctness, whereas with seL4 it actually is shown that a kernel call meet some formal requirement.
- 3y ago
- collegeburner 3y agobeing so real rn i thought this was an llm (insert skull emoji) twitter is breaking me might be helpful to change the title to integrity-178 since that appears to be the OS' name while DO-178B is a standard
- Philpax 3y agoI’ll admit I had the same impression at first. [name]-[number]B is a very common convention for referring to LLMs now!
- ThinkBeat 3y agoI wish it was open source.
- AlotOfReading 3y agoNot only is green hills stuff not open source, the contracts typically include a clause preventing you from compiling open source with their toolchain.
- IAmLiterallyAB 3y agoWhy would they care about that...
- zebomon 3y agoFrom my understanding, it's generally the same reason they have made the kernel exceptionally small -- to reduce attack surface.
- foobiekr 3y agoIt makes liability for failure more complicated and customers might link their proprietary items to toxic licenses. They don’t want to be involved. Also, just to be frank, if you’re using a solution like this, open source does not meet your requirements.
- AlotOfReading 3y agoNo, it's because open source competes with some of their upsell offerings and they want to preserve their auxiliary sales. As for whether it meets your requirements, that's entirely dependent on context. In most cases it's a perfectly valid choice as long as you understand that you're taking on the associated maintenance and certification burden. In our case, it included stuff we had written and open sourced ourselves.
- mighmi 3y agoThe Thompson attack's where code is able to secretly modify/exploit the compiler to propagate through future compiled programs or itself when compiled. Preventing the execution of foreign code thus reduces the attack surface even further.
- cookiengineer 3y agoI always wonder how safety critical software is certifiable without any source code. Checklist security, I guess.
- Veserv 3y agoBecause the entity doing the certification has access to the source code (if the certification is worth anything at all) and if you really do not trust the certification body you can usually just pay extra for access to the source code without distribution rights and do it yourself. For instance, even Microsoft has the Shared Source Initiative [1] which allows qualified customers access to their source code. [1] https://www.microsoft.com/en-us/sharedsource/ https://www.microsoft.com/en-us/sharedsource/
- girvo 3y ago...because its not certified without any source code lol. You hand the whole source tree (and more!) over. I must be misunderstanding your point!
- wyager 3y agoThe public behavior of their CEO makes me very skeptical of their public claims about this OS. The CEO has tons of tweets along the lines of (not really exaggerating) "my OS is perfect and cannot be hacked. I have XYZ certification. I used to work on nukes." These are not the words I expect from someone who has actually written a meaningfully "unhackable" OS. I expect discussion of e.g. theorem proving strategies, logic systems, etc., not NIST ABC-123 certs.
- chmorgan_ 3y agoLast system I worked on with GHS Integrity was something like a USD $1M+ licensing fee. In terms of usage, it felt like it was in between an RTOS like FreeRTOS, embossed, or Zephyr, and Linux. It used a lot of best practices like statically allocating memory for basically everything, so you knew you had sufficient memory (at least for anything the OS needed) when your application was loaded.
- fargle 3y agoso the problem with "DO-178" OS like vxWorks or ghs is that it's not DO-178. it's a version of the OS that has artifacts to support getting your produce DO-178 certified using it. It's DO-178 "certifiable" maybe. if you need to certify one million lines of OS and a 1/2 million lines of your application, it's handy to have that first bit done for you. Until you find that you have a 1/2 million lines of code that interface with the OS. so we're _done_ with this crap. say we have a 1/2 million lines of our application and 50,000 lines to talk to our hardware, and less than 10,000 for a simple executive. I don't need your scheduler (which doesn't work right), your compilers (which are just buggy old out-of-date ports) or your IDE which is just buggy, old, out-of-date eclipse with a plugin and branding. And I don't need your DO-178 artifacts for a million lines of buggy OS code when I can replace it with less code than that it takes to interface with your bug riddled OS. And when you buy the DO-178 version, don't think it means "has less bugs". DO-178 means that it has specific artifacts including MCDC coverage against requirement based tests. All of that is very expensive. None of that means it works right. If you put your money into checklists and process, guess how much is left for "making it work right". Garbage. If you are responsible for safety-critical software, then you are responsible for safety-critical software. Paying a 3rd party for part of the responsibility would be nice if they took any responsibility, which they don't. So, in conclusion: Pbththththh!!! on the snake oil vendors of safety magic.
- Veserv 3y agoWhat a bizarre take. Basically every serious commercial and military aircraft design and systems upgrade in the last 20 years voluntarily uses a third party RTOS for basically all critical flight systems demanding a DAL Level A certification. Those same certified systems have never once been implicated in a single commercial aviation fatality over those 20 years resulting in 9-12 9s of software reliability (depending on how you count) for those software components which is positively ludicrous in comparison to what is considered the gold standard in regular commercial IT software. You also assert technical specifications that bear no resemblance to normal reality in the field such as 1 million lines of OS (you are generally off by a factor of 10 to 100 depending on vendor) or 1/2 million lines to interface (again, off by a factor of 10 to 100). Maybe such a thing might happen when working with a second rate vendor who does not have any real proven history or actual in-house expertise at making high criticality systems selling you a bill of goods about "certifiability"?