Conversation

This Tweet was deleted by the Tweet author. Learn more

Replying to

No, that's not what he means. He's saying that an external file system should have a sandboxed filesystem driver, so that exploiting a bug inside it doesn't immediately grant complete control over the entire system and at least requires privesc to escape (likely via the kernel).

Replying to

Try reading the overview in events.linuxfoundation.org/wp-content/upl. Finding a Linux kernel vulnerability is not hard. Literally hundreds of bugs are found by syszkiller every month and many are not fixed. Most are memory corruption. There are simply too many to even fix all discovered bugs.

Replying to

yes, we don't need to debate the question "can people write memory safe code in C" the answer is overwhelmingly obvious to almost all of us

Replying to

It would be hard enough to make a microkernel secure if it was 50k lines of Rust with only 4k lines of unsafe code with potential memory corruption, let alone millions of lines of trusted C full of memory corruption from all kinds of trivial mistakes / oversights. It's a joke.

Replying to

Just want to point out that seL4 is about 10K lines of C and is formally verified to use no UB, no OOB array access, no crashes, etc... Not trying to defend C but there are ways to make anything safe if you care enough. The problem is people don’t care.

Replying to

Sure, but at that point it's not C. It's a subset of C that was verified via proofs. Those proofs are an extension to the language. Similarly, you can define a general purpose subset of C with annotations for ownership, lifetimes, etc. letting you write memory safe code.

Replying to

You end up with something that looks a lot like Rust. You can't compile existing C codebases with an implementation of it. They have to be specifically written for it with the annotations, but they don't need complex proofs, unless they want to prove more than memory safety.

Replying to

No, it doesn't look at all like Rust. It has completely different idioms and is much simpler. There's no such thing as "an implementation of it" that can't compile existing codebases because it's just C.

Replying to

The choice to use a particular good form of the language is on the application side, not the implementation side.

Replying to

It does end up looking like the memory safety system in Rust if you are actually introducing a system to provide memory safety. The kind of clean C code you are talking about still has plenty of memory corruption bugs and is still unacceptable for modern security requirements.

12:47 AM · Apr 18, 2019Twitter Web Client

Replying to

You absolutely don't "introduce a system". That's anti-idiomatic and just reconstructing some other heavy language on top of C, which is always awful.

Replying to

By introduce a system, I mean defining a subset of C with annotations that is actually memory safe, which isn't all that complex and doesn't need to have much noisy syntax. A lot can be inferred, but still, you can't easily adapt existing code to be verified as safe like this.

Show replies