4 ms·

here other approaches to secure them actually work, like sandboxes and containers, "It is a fallacy to think that for 30+ years people haven't b

here other approaches to secure them actually work, like sandboxes and containers, "It is a fallacy to think that for 30+ years people haven't been able to write a secure OS. But virtualization, and containers are" - Theo de Raant

nickpsecurity 10y ago
GEMSOS, KeyKOS, ASOS, LOCK, VAX VMM, INTEGRITY-178B, seL4, NOVA... all in the 4Kloc-50+Kloc range for a reason. All simpler, smaller, and easier to model than a full OS. Two survived pentesting by NSA with others during validation way better in defect rate or correctness case than most OS's. Theo's quote is BS by the numbers and pentest results. Sandboxing done right is way more secure.
- lobster_johnson 10y ago
  While true, in practical terms, those OSes are not what people have lying around to do their image processing. I'd love a secure, formally verified, capabilities-based microkernel OS as much as next person, but all I have is Linux and various BSDs. It's a bit academic at this point.
  - nickpsecurity 10y ago
    The commenter countered that sandboxing was worthwhile by citing a claim by Theo de Raadt that getting those (i.e. VM's) right was about as hard as getting whole OS's of code right. That one proved futile meant the other would. I countered that citation with numerous examples that disprove his point. Then, by implication, sandboxing might be effective if it's done like in my examples. And there are CompSci designs doing stuff like that. Whether you want to do image processing on a Linux, BSD, or one of my kernels is a separate topic. However, it's worth noting that even stuff like I cited could be useful for that where it stashes the image processor into its own protection domain with read access to memory containing input and write access to memory that will have the output. The code itself isn't allowed to do or touch anything else. At this point, exploits must be chained in clever ways. Modifying this to preserve pointer integrity, lowest overhead range being around 1-10%, would choke those kind of attackers further. Using Rust is yet another tactic that can work well with or in lieu of a sandbox. Ideally with for issues the language itself can't cover. Three precedents for that are right on my list: GEMSOS's safety was improved using a Pascal subset with call-by-value semantics; ASOS was a combo of security kernel and Ada runtime to host embedded, Ada applications (lang-safety + sandbox); separation kernels like INTEGRITY-178B usually support runtimes for Ada and Java subset to get safety within components. Now, there's some OS's like Tock and Redox plus low-level libraries written in a new, safety-enhancing language. Such designs can benefit from the old strategies which we see a few in Redox. On other end, Genode uses many old and recent tricks in architecture but not safe language. It can also run a Linux desktop with your image processing code. ;) Note: A bit academic is also misleading. Several, separation kernels are deployed commercially for things like secure, web browsing. INTEGRITY and LynxSecure are among oldest. The Nizza and Perseus architectures got turned into Sirrix's Turaya Desktop. These things aren't just academic.
    - valarauca1 10y ago
      Then, by implication, sandboxing might be effective if it's done like in my examples. And there are CompSci designs doing stuff like that. I mean it is great if you can wave your hands and invent a Hoarce Logic proof your code is secure. But your Hoarce Logic models hardware. While you can prove your Hoarce Logic is consistent you can't prove your Hoarce Logic maps to existing hardware. You can only ensure the review board you made your best effort. Which defeats the exercise completely.
      - nickpsecurity 10y ago
        You could argue against safety of Rust, OpenBSD, etc. with the same strawman. What it and those kernels did were creating an abstract model realistic enough to be useful, embed a safety/security policy in that model, and produce code that corresponds to that model. Older systems used what's called Abstract, State Machines which are quite easy to model-check or even analyze by hand. Typically converted to FSM's with same advantage. It was usually done by hand and eye instead of formally. In GEMSOS, the Gypsy specs mapped to code's functions/modules about 1-to-1 in most cases. Recent efforts did it formally for things ranging from kernels to application-layer sandboxes. In case of VCC and SPARK, they do annotations on the code itself. In things like seL4, they do proofs on the code connecting it to a model. So, one can do that. It's usually not necessary since we're talking about improving the security of things over the status quo. You seem to be adding an additional requirement of totally unhackable with mathematical proof down to the hardware. AAMP7G and SSP are production CPU's close to that, esp AAMP7G. VAMP with CodeSeal & CHERI might do it, too. One academic one was proven down to the gates. They're all irrelevant as we're talking about reducing damage of an image library on regular CPU's & OS'. You trust the Rust typesystem, compiler, and optimizations were implemented correctly enough that they'll knock out a bunch of problems. Certifying compilers like FLINT & CompCert took mountains of verification effort to pull off a fraction of that. Whereas, I'm saying one can trust 4-12Kloc or a compiler transformation connected to an abstract model fitting on a page or two might do its job with fewer problems than trusting just complex, native code in C or whatever. I also encourage mixing such TCB's with language-based security. However, such a tiny, clean, ASM-style program will have way fewer defects than a full OS or application.
kod 10y ago
That's a hilariously appropriate typo in the spelling of his last name.
lmm 10y ago
If you squint then containerisation looks rather like the minimalistic microkernels which have formed the few genuinely secure OSes of those 30+ years.

nickpsecurity 10y ago

GEMSOS, KeyKOS, ASOS, LOCK, VAX VMM, INTEGRITY-178B, seL4, NOVA... all in the 4Kloc-50+Kloc range for a reason. All simpler, smaller, and easier to model than a full OS. Two survived pentesting by NSA with others during validation way better in defect rate or correctness case than most OS's. Theo's quote is BS by the numbers and pentest results. Sandboxing done right is way more secure.

lobster_johnson 10y ago
While true, in practical terms, those OSes are not what people have lying around to do their image processing. I'd love a secure, formally verified, capabilities-based microkernel OS as much as next person, but all I have is Linux and various BSDs. It's a bit academic at this point.
- nickpsecurity 10y ago
  The commenter countered that sandboxing was worthwhile by citing a claim by Theo de Raadt that getting those (i.e. VM's) right was about as hard as getting whole OS's of code right. That one proved futile meant the other would. I countered that citation with numerous examples that disprove his point. Then, by implication, sandboxing might be effective if it's done like in my examples. And there are CompSci designs doing stuff like that. Whether you want to do image processing on a Linux, BSD, or one of my kernels is a separate topic. However, it's worth noting that even stuff like I cited could be useful for that where it stashes the image processor into its own protection domain with read access to memory containing input and write access to memory that will have the output. The code itself isn't allowed to do or touch anything else. At this point, exploits must be chained in clever ways. Modifying this to preserve pointer integrity, lowest overhead range being around 1-10%, would choke those kind of attackers further. Using Rust is yet another tactic that can work well with or in lieu of a sandbox. Ideally with for issues the language itself can't cover. Three precedents for that are right on my list: GEMSOS's safety was improved using a Pascal subset with call-by-value semantics; ASOS was a combo of security kernel and Ada runtime to host embedded, Ada applications (lang-safety + sandbox); separation kernels like INTEGRITY-178B usually support runtimes for Ada and Java subset to get safety within components. Now, there's some OS's like Tock and Redox plus low-level libraries written in a new, safety-enhancing language. Such designs can benefit from the old strategies which we see a few in Redox. On other end, Genode uses many old and recent tricks in architecture but not safe language. It can also run a Linux desktop with your image processing code. ;) Note: A bit academic is also misleading. Several, separation kernels are deployed commercially for things like secure, web browsing. INTEGRITY and LynxSecure are among oldest. The Nizza and Perseus architectures got turned into Sirrix's Turaya Desktop. These things aren't just academic.
  - valarauca1 10y ago
    Then, by implication, sandboxing might be effective if it's done like in my examples. And there are CompSci designs doing stuff like that. I mean it is great if you can wave your hands and invent a Hoarce Logic proof your code is secure. But your Hoarce Logic models hardware. While you can prove your Hoarce Logic is consistent you can't prove your Hoarce Logic maps to existing hardware. You can only ensure the review board you made your best effort. Which defeats the exercise completely.
    - nickpsecurity 10y ago
      You could argue against safety of Rust, OpenBSD, etc. with the same strawman. What it and those kernels did were creating an abstract model realistic enough to be useful, embed a safety/security policy in that model, and produce code that corresponds to that model. Older systems used what's called Abstract, State Machines which are quite easy to model-check or even analyze by hand. Typically converted to FSM's with same advantage. It was usually done by hand and eye instead of formally. In GEMSOS, the Gypsy specs mapped to code's functions/modules about 1-to-1 in most cases. Recent efforts did it formally for things ranging from kernels to application-layer sandboxes. In case of VCC and SPARK, they do annotations on the code itself. In things like seL4, they do proofs on the code connecting it to a model. So, one can do that. It's usually not necessary since we're talking about improving the security of things over the status quo. You seem to be adding an additional requirement of totally unhackable with mathematical proof down to the hardware. AAMP7G and SSP are production CPU's close to that, esp AAMP7G. VAMP with CodeSeal & CHERI might do it, too. One academic one was proven down to the gates. They're all irrelevant as we're talking about reducing damage of an image library on regular CPU's & OS'. You trust the Rust typesystem, compiler, and optimizations were implemented correctly enough that they'll knock out a bunch of problems. Certifying compilers like FLINT & CompCert took mountains of verification effort to pull off a fraction of that. Whereas, I'm saying one can trust 4-12Kloc or a compiler transformation connected to an abstract model fitting on a page or two might do its job with fewer problems than trusting just complex, native code in C or whatever. I also encourage mixing such TCB's with language-based security. However, such a tiny, clean, ASM-style program will have way fewer defects than a full OS or application.

kod 10y ago

That's a hilariously appropriate typo in the spelling of his last name.

lmm 10y ago

If you squint then containerisation looks rather like the minimalistic microkernels which have formed the few genuinely secure OSes of those 30+ years.