[HN Gopher] Integrity-178B: Safety Critical Real-Time OS
___________________________________________________________________
Integrity-178B: Safety Critical Real-Time OS
Author : veqq
Score : 29 points
Date : 2023-12-02 16:15 UTC (6 hours ago)
(HTM) web link (www.ghs.com)
(TXT) w3m dump (www.ghs.com)
| Animats wrote:
| Green Hills Software? They're still around, and doing good
| things? That's impressive.
| f1shy wrote:
| Around, yes. Doing good things... ehm well, they do things, not
| the best, and are arrogant as hell.
| KRAKRISMOTT wrote:
| Weren't they the ones who sued tesla?
| mips_r4300i wrote:
| VxWorks wants know your location...
| joezydeco wrote:
| Whereas Green Hills wants to see your accounting books.
| jtwaleson wrote:
| The 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 wrote:
| this?
|
| https://www.motortrend.com/features/tesla-full-self-
| driving-...
| veqq wrote:
| What do you mean by arrogant as hell? I'd not heard much
| about them.
| GnarfGnarf wrote:
| How much is a license for their OS?
| AlotOfReading wrote:
| Enterprise 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 wrote:
| Last 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 wrote:
| However much you can pay. Millions. Not even joking. It may be
| worth it for a big ticket aircraft program though.
| johnea wrote:
| If you have a large gov contract for incinerating the poor, this
| is the OS for you...
| Veserv wrote:
| You can see the SKPP certification requirements here:
| 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_vid103...
|
| You can see the certification report here:
| 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 wrote:
| It 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.
| veqq wrote:
| Do you have experience working with such systems? I'd love to
| drink deeply of your knowledge if possible, past experiences,
| interesting technologies, how to start, the big players in safe
| systems etc.
|
| I've seen PikeOS, LyncSecure and VxWorks also. There's an
| interesting related book Embedded Systems Security and... I
| suppose I should investigate Ada etc.
| inamberclad wrote:
| A lot of them provide normal-ish C programming environment.
| Files, network sockets, etc. the virtual memory space
| isolation is a huge feature that's hard to certify, so Green
| Hills is leading the field there.
| collegeburner wrote:
| being 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
| ThinkBeat wrote:
| I wish it was open source.
| AlotOfReading wrote:
| Not only is green hills stuff not open source, the contracts
| typically include a clause preventing you from compiling open
| source with their toolchain.
___________________________________________________________________
(page generated 2023-12-02 23:00 UTC)