Hacker News Reader

> having optimizations off is not an option either, since it can generate broken code as well, so...

Especially when you add this line, you're telling me that what you want is not to program in C but to program in a language which differs from C not in syntax but in semantics, and in otherwise vaguely undefined terms [1] there. And you're mad that compilers implement C instead of your not-C.

I find claims that you can safely write secure code in C hard to believe when you marry them with complaints about compilers not implementing not-C correctly. Especially given that virtually every new sanitizer and static analysis tool to find issues in C code manages to turn up issues in code that is rigorously tested to make sure it passes every known prior tool (e.g., SQLite).

[1] From prior experience, this tends to be best distilled as "the compiler must read the programmer's mind."

It is not possible to remove ub from the spec without turning everything into a pdp-11 emulator, which will sabotage performance on many platforms.

I also don’t believe that a single person on the planet can write a secure c program of meaningful complexity. Static analysis tooling has demonstrated that it isn’t up to the task of saving developers from themselves.

What about SEL4?

Written over many many years by experts of a field, and the end result is at most somewhat complex, nowhere near the complexity of even the monolith SPA of your favorite website.

GP said:

> meaningful complexity

Not, "the most complex". If an OS that can lock down DARPA self-flying helicopter software is not meaningful enough for you....

Less than 10 000 lines of code. But let’s say we accept it as an exception — it is most definitely not the “standard way” of writing C programs.

From GP:

> It is not possible to remove ub from the spec

did not say "it is not standard to remove ub"...

The speed of development was very low, and how many people can check the proofs?

> The speed of development was very low,

Not a part of GP's assertion

> and how many people can check the proofs?

it's not necessary, the proofs are checked using automation. I'm directly taking a shot at this assertion:

> Static analysis tooling has demonstrated that it isn’t up to the task

Just because you have a proof doesn't mean it proves the right thing.

Congratulations. You have won the argument "there is no perfectly secure system", which no one was arguing.

I've got a strong background in formal verification. I do not believe that "formally verified" means "security bug free". In fact, I personally know researchers who have had vulns found in their formally verified code more than a decade after they completed the verification.

I don't think there is any reasonable standard of security that demands perfection.

I agree, there are lots of outrageous claims out there about "provably secure software" which seem very dubious.

What are your thoughts on SEL4, is it really a breakthrough it is made to be in success of formal verification? Is there a way for users/administrators deploying it to verify themselves authors' claims? Or is it too difficult? I am afraid the latter...

In 2004 Peter Gutmann in his thesis/book criticized the hype around effectivity of formal methods in computer security [1]. Has the situation changed?

[1] https://archive.org/details/springer_10.1007-b97264

Breakthrough? No. Good work? Yes.

> I've spent 10 years writing security critical C code. There's no problem writing secure code in C. You just have to stop being clever and prioritize security above "speed". Your code will probably be fast enough anyway.

Are there good examples of what you mean by this? From my own C++ experience, when dealing with c libraries and std::string types, I'll sometimes use the copying api's[0] when passing around std::string::c_str() because I find it easier than worrying about invalidating the returned reference if the string is destructed or modified.

[0]: e.g. https://curl.se/libcurl/c/CURLOPT_COPYPOSTFIELDS.html

Which checks will the compiler remove? If you haven't invoked undefined behaviour then that should be a bug in the compiler

They might be thinking of cases like where C compilers can remove code that zeroes memory holding security-sensitive data. [0][1] The compiler is permitted to reason that this memory is about to be deallocated anyway, so we can elide the memset call.

I can't imagine why a C compiler would remove a non-trivial runtime check though (except undefined behaviour).

[0] https://wiki.sei.cmu.edu/confluence/display/c/MSC06-C.+Bewar...

[1] https://lists.isocpp.org/sg14/2020/12/0482.php

If there were no problem writing secure code in C and C++ we would have a lot fewer vulnerabilities based on some form of memory corruption.