[quasit1]

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.

If it's too slow, then you probably have an issue with which algorithm/data structure you chose and would have had the same issue in another language.

The biggest issue I have with C today is that you can't trust that your compiler actually generates code that is 1:1 with what you wrote. I'm not talking about UB here, your compiler can actually remove code/checks even though you don't invoke UB.

Then we have UB, I think UB should be removed from the spec completely. There probably was a point in time when leaving stuff as UB was the best option, but today speed is seldom the problem, correctness is.

I no longer work as a C programmer, but I still love the language and I really enjoy writing C code, but I really would like to get rid of UB and have a compiler I can trust to generate code even when I turn on optimizations, and having optimizations off is not an option either, since it can generate broken code as well, so...

[jcranmer]

> 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."

[UncleMeat]

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.

[dnautics]

What about SEL4?

[kaba0]

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.

[dnautics]

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....

[kaba0]

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.

[dnautics]

From GP:

> It is not possible to remove ub from the spec

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

[posix_me_less]

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

[dnautics]

> 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

[oscardssmith]

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

[dnautics]

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

[UncleMeat]

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.

[posix_me_less]

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

[UncleMeat]

Breakthrough? No. Good work? Yes.

[dnautics]

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

[prussian]

> 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

[mhh__]

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

[MaxBarraclough]

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

[adrianN]

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.