4 ms·
> C cannot be made safe because you are not a god I mean this is demonstrably untrue: SEL4 is written by mere mortals, in C. It's safer than rust, there are f
by throwawaymaths 4y ago
> C cannot be made safe because you are not a god
I mean this is demonstrably untrue: SEL4 is written by mere mortals, in C. It's safer than rust, there are formally verified security guarantees that include and go beyond the memory safety of rust.
It is the case though that c is an incredibly shitty language to do this sort of static analysis on because for example it's easy to do shenanigans like lexical macros that make the static analyzers job much much harder.
- vore 4y agoseL4 also has the whole Isabelle/HOL theorem prover to verify its properties, so it's not quite right to claim it's written in C. If you can claim seL4 is "written in C", you could equally claim that if the Rust compiler emitted C, you're writing a C program -- after all, a static type checker is just a shittier theorem prover.
- throwawaymaths 4y agoThis is like saying <insert language with docstrings> is not actually writing in <lang> because you need whatever engine's target language (md, XML, whatever) to compile the docs.
- avgcorrection 4y agoThat comparison is nonsensical and you know it. You can delete all the comments and have the same guarantees about what the code does (none). You can’t write a kernel without some formal verification tool and then claim that it adheres to the specification.
- throwawaymaths 4y agoNo, but if you change none of the code and only delete the annotations, it will still adhere to the spec.
- avgcorrection 4y agoOh, I see. You said that it is “written in C”, and then later denied the claim that it is also written with that formal verification language. If you delete those annotations it will still adhere to the specification,[1] but it’s still false that it was purely written in C—your statement that “there are formally verified security guarantees” in fact relies on the existence of that proof code. But fine. With that kind of dishonesty I could claim that the Linux kernel is written in nothing: I have compiled it and deleted the source code. Look ma, it’s no-code kernel. [1] Kind of a bummer though that you cannot change any of the C code any more now that the verification code is gone.
- throwawaymaths 4y agoJesus Christ. It's not like most c programs arent already written in another language like make or cmake. By your standards none but the most trivial of hello world a.out c programs are c programs.
- renox 4y agoAnd C is also AFAIK the only language with a formally proven compiler CompCert C. If you used something else, you'd need to trust a lot more code.
- vore 4y agoCompCert doesn't stop you from writing memory unsafe C, of course, just that it won't miscompile your maybe memory unsafe C.
- aw1621107 4y ago> And C is also AFAIK the only language with a formally proven compiler CompCert C. There's CakeML, which is a formally verified subset of Standard ML [0] [0]: https://cakeml.org/popl14.pdf https://cakeml.org/popl14.pdf
- kobebrookskC3 4y agocuriously, seL4 doesn't need to trust the compiler: the assembly is verified to satisfy the abstract specification
- yaantc 4y agoMacros are not such a big deal: static analyzers do not work on the source code directly, they work on some intermediate representation usually (often the LLVM IR, for Ikos and Clang SA for example) or parsed source code. Either way, the pre-processing has been done when the analysis starts. Funky macros can still make static analysis more complex by introducing layer(s) of indirection of course.
- kstenerud 4y agoYou can make any code in any language "safe" when you throw enough resources at it. That's not an argument for safety, nor a rebuttal (unless your goal is to prove someone wrong on the internet).
- throwawaymaths 4y agoOk but please acknowledge that this comment is explicitly the opposite of "you cannot make c safe ever"
- kstenerud 4y agoIt's the exact opposite of "you cannot make language X safer", only if you define that as "given enough time and resources, you could make a proof that your program is correct". But that's not a safe language; that's a safe work. ANY programming work - regardless of language - can be made safe via such expensive means, which puts this square into the space of "argument ad absurdum". You could argue that brainfuck or assembler can be made safe via these means, but everyone would rightly ridicule you for it.
- throwawaymaths 4y agoMaybe I'm crazy but "being a god" is much higher bar than "given enough time and resources, you could make a proof that your program is correct". Moreover, unlike your bf analogy: Sel4 exists, and is in use, and is used in safety-critical applications such as military drones.
- kobebrookskC3 4y agoit's also a very limited version of C, without concurrency, dynamic memory allocation, or goto, and you can't even take the address of local variables!