Comment by mafribe | Hacker News Reader

Comment by mafribe | Hacker News Reader

Parent Full thread

True, seL4 verification doesn't solve the application level security problem but it makes it more approachable in several ways.

- No longer need the verification of application make assumptions about the semantics of the operating system. Instead, concrete and verified semantics are available. This makes application specification and verification easier, and safer. Fortunately, verification is cumulative

- The seL4 project has driven the state-of-the-art of verification tool forwards by a considerable degree.

- The seL4 project has lead the thinking about proof engineering [1], the emerging field that that is to verification what software engineering is to programming, addressing the question how to develop, maintain and evolve large-scale proofs.

- The existence of something like seL4 also puts pressure on CPU manufactures to provide usable formal specifications to their customers, so that we can verify against rigorous CPU specs. CPU manufacturers have been loath to do this (for various reasons).

The full verification of seL4 came a lot earlier (by about a decade) than I thought possible.

[1] G. Klein, Proof Engineering Considered Essential.

What's your sense of the number of IoT vulnerabilities that are due to misconstrued OS semantics? Mine --- and I've done a bit of work here, but not that much --- is that there aren't that many.

Really I think it depends on what you're doing. If the work you're doing is fundamentally kernel work --- if it's all about interacting with the security boundaries of the hardware (not just "interacting with hardware", like getting the bits from an RF codec, but manipulating hardware shared by attackers, like the iPhone SEP) then L4 is a pretty huge security win.

Otherwise: the problem you have isn't your OS, but the programming language you're using to build with.

I'm happy to believe that almost all IoT vulnerabilities are application level problems.

The beginning availability of verified kernels and compilers makes it much more worthwhile to invest in formal approaches for application level vulnerabilities.

See my comment. It has top approaches to that which already delivered implementations.

'Not that many' is not really acceptable for many applications, and I'm not talking only about IoT, but self-driving cars, surgery robots, rockets, etc.

If done well, formal verification of kernel level services and how these use runtime protection built in hardware can absolutely reduce the attack surface of application level code. The key is to move critical services that attackers would wish to exploit into a formally verified sandbox. That is the real power of systems like seL4, even though seL4 isn't itself really geared toward the sort of chipsets commonly used in consumer grade IoT products. However, a system _like_ seL4 can absolutely improve application level security, as long as the application is constrained by the architecture of the OS.

Can you describe this with an example of a realistic use of L4-enabled sandboxing for a single-function IoT device?

(I've done some L4 work so you don't need to spend a lot of time explaining.)

General purpose OSs like iOS? No question: L4 is a major win. But that's not what the discussion here is really about.

Case in point: cryptography, authentication, and authorization are each very sensitive operations which are prone to both gadget attacks and sidechannel attacks. Sandboxing these operations by creating well-defined boundaries between application code and these algorithms and protocols can ensure that application level bugs cannot creep into these critical services.

Consider, for instance, that it is possible to separate TCP/IP or wireless protocol stacks from authentication code so that, for instance, a packet fragmentation bug can't be exploited to influence authentication level decisions. This is classical defense in depth strategy, but enforced through both runtime and formal methods.

You wouldn't, SEL4 isn't designed for embedded systems. That's what NICTA's eChronos [1] is for : )

1: http://ts.data61.csiro.au/projects/TS/echronos/

seL4 is designed for embeddee systems. That's why it mainly targeted ARM. Gernot Heiser even said so. I believe eChronos is just targeted for embedded devices with more constrained hardware.

> I believe eChronos is just targeted for embedded devices with more constrained hardware.

I guess it all depends on which meaning of IoT and embedded you are using.

No MMU is usually the differentiating constraint when there's two RTOS's. I dont use IoT because it's a BS buzzword.

IoT isn't really target for these things. Language or spec-level security is more important. I agree with you there. Isolation mechanisms are still important for many embedded devices, though, if security is a concern. Here's a few I've seen in various products or academic programs:

1. Device driver isolation. Wacky drivers can take down the system. Better to take down and restart the driver. QNX was first I know of that did this with excellent reliability benefits. Many of them do now in RTOS space. MINIX 3 takes it to desktops and servers.

2. Monitors like in Copilot system or for recovery-oriented computing that expects input to crash or subvert main process. So, outside process is necessary for detection of anomalous behavior and recovery. Periodic restarts are another trick used in that field to clear out subtle errors that build up over time or persistent malware. Best to be in different address spaces.

3. Dedicated process, as in Nizza and Turaya, for containing application secrets where external processes can call to have random numbers generated, signatures performed, etc but not actually access the internals.

4. Same thing for logging purposes where interface between main app and logging component is write-only. Prevents accidental or malicious elimination of audit trail. I did that myself many times. Shapiro et al did it for repo security.

5. Finally, separation kernels like INTEGRITY-178B can ensure predictability of certain operations and statically enforce a scheduling policy. That's important in real-time systems where a number of tasks are running where one can screw with the other. So, they use things like ARINC schedulers with fixed-sized partitions operating in fixed intervals. Watchdog timers are also popular here. Also is a strategy for eliminating covert, timing channels at partition level for select few that need that.

The problem is it takes more than just implementing the "kernel" (as in low-level access aka HAL) work under L4. You need to apply that compartmentalization all the way through the stack, and even subdivide applications into smaller chunks of responsibility.

What you typically get is a neat subdivision of all the HAL bits, but everyone stops once they're plugging in applications. This is partly because there's normally a large amount of shared/legacy code which needs importing, and partly because people don't recognize the benefits of partitioning an app.

It's not all bad - at least you can be reasonably confident that one compromised app, or part of the HAL, can't be trivially used to compromise the rest of the system. But, as you say elsewhere here, if there's just one thing you're doing, then all that effort didn't really improve things.

I wonder if anyone will manage to create a tool for Rust that can map out code partitions, or near partitions, based on access patterns of object ownership. At some tipping point a little bit of data sharing could be refactored into message passing and finish the job right.

> The full verification of seL4 came a lot earlier (by about a decade) than I thought possible.

Is it a full verification yet? I am by no means an expert, but IIRC, they were still using a simplified model MMU in their proofs.

It's a simplified model, but it's well validated. Without connecting the proofs to a formally verified chip, it's about the best you can do.

Reply on news.ycombinator.com