TrustInSoft Blog

I still want to write at least one sequel to that post, on the theme “Alright, can we make a Friendly C Compiler by disabling the annoying optimizations, then?”.

Obviously the people who want a Friendly C Compiler do not want to disable all optimizations. This would be easy to do, but these users do not want the stupid 1+2+16 expressions in their C programs, generated through macro-expansion, to be compiled to two additions with each intermediate result making a round-trip through memory.

So the question is: can we get a Friendly C Compiler by enabling only the Friendly optimizations in an unfriendly compiler?

And for the answer to that, I had to write an entire other blog post as preparation, to show that there are some assumptions an optimizing compiler can do:

- that may be used in one or several optimizations, but the compiler authors did not really keep track of where they were used,

- that cannot be disabled and that the compiler maintainers will not consider having an option to disable,

- and that are definitely unfriendly.

Here is the URL of the blog post that I had to write in preparation for the upcoming blog post about getting ourselves a Friendly C Compiler: https://trust-in-soft.com/blog/2020/04/06/gcc-always-assumes-aligned-pointers/ . I recommend you take a look, I think it is interesting in itself.

You will have guessed that I'm not optimistic about the approach. We can try to maintain a list of friendly optimizations for ourselves, though, even if…

So, any experience reports?

I can recommend https://www.imperialviolet.org/2014/09/07/provers.html.

Personally, I tried to prove that a fairly simple program I had written a few years prior was free of undefined behavior. Frama-C was tantalizingly capable - it was easy to tell Frama-C what I wanted to prove, and it managed to propagate possible values and control flow through the program pretty accurately, even with minimal assistance. Although I disliked the absence of a usable text-mode integration (vim?), the GUI presented the results clearly. The Frama-C manuals were extensive, mostly up-to-date, and managed to explain even complicated concepts in a pretty clear way. (Fair warning: although I have zero background in formal methods, I have quite a lot of mathematical training and like language lawyering.)

Unfortunately, Frama-C did not grok malloc() at the time. My program consisted of I/O into malloc()'ed buffers plus some processing. Teaching Frama-C about malloc() was clearly beyond my skill. Worse, I really wanted to prove that my program output was some suitably processed form of its input data, and I didn't look forward to trying to model read()/write() - so I stopped the experiment, and planned to revisit Frama-C in a couple years.

Actual experts can apparently get much better results: Frama-C was used to prove that chunks of PolarSSL were free of certain undefined behavior (http://blog.regehr.org/archives/1261, or the actual report at…

No, ssize_t is not the signed version. As best as I can tell, the only things POSIX says about ssize_t is that[1] it is an integer type that can hold integer values in [-1, SSIZE_MAX], where[2] SSIZE_MAX ≥ _POSIX_SSIZE_MAX = 32767, not that it should have any particular relation to size_t. In the standard, it is used for byte counts in I/O, like the return value of read() (traditionally int), for the return value of strfmon() and strfmon_l() (OK I guess, though the C standard stuck with int for *printf()), and for the argument to swab() (wat).

Note that neither is ptrdiff_t guaranteed to be that signed version, or to hold any possible value in the domain of size_t or (strictly speaking) any possible object size. Both GCC and Clang assume the latter, though, and can miscompile[3] code that relies on (e.g.) malloc() succeeding for sizes > 2^31 on a 32-bit system.

[1] https://pubs.opengroup.org/onlinepubs/9699919799/basedefs/sys_types.h.html

[2] https://pubs.opengroup.org/onlinepubs/9699919799/basedefs/limits.h.html

[3] https://trust-in-soft.com/blog/2016/05/20/objects-larger-than-ptrdiff_max-bytes/

No, I haven't kept track of the reports I've seen. They all had array bounds as the #1 error encountered in shipped code.

Edit: I just googled "causes of memory safety bugs in C++". Number 1 answer: "Buffer Overflows/Out-of-Bounds Access"

"Undefined behavior in C/C++ code leads to security flaws like buffer overflows" https://www.trust-in-soft.com/resources/blogs/memory-safety-issues-still-plague-new-c-cpp-code

"Some common types of memory safety bugs include: Buffer overflows" https://www.code-intelligence.com/blog/memory_safety_corruption

"Memory Safety Vulnerabilities 3.1. Buffer overflow vulnerabilities We’ll start our discussion of vulnerabilities with one of the most common types of errors — buffer overflow (also called buffer overrun) vulnerabilities. Buffer overflow vulnerabilities are a particular risk in C, and since C is an especially widely used systems programming language, you might not be surprised to hear that buffer overflows are one of the most pervasive kind of implementation flaws around." https://textbook.cs161.org/memory-safety/vulnerabilities.html

Two others worth checking out that focus on soundness with low to no false positives are RV-Match and TrustinSoft Analyzer:

https://runtimeverification.com/match/

https://trust-in-soft.com/products/

The RTV people are the one's behind K framework and an executable semantics for C with a GCC-like interface:

http://www.kframework.org/index.php/Main_Page

https://github.com/kframework/c-semantics

That RV-Match builds on an open framework, does well on benchmarks (yeah skepticism here), and has little to no noise (most important) is what I like most about it. I say most important since digging through false positives makes developers not want to use a tool. I haven't tried either product myself, though.

Here's a list of open tools that did well in small-scale experiments with and without false positives:

https://klee.github.io

http://www.cprover.org/cbmc/

https://cseweb.ucsd.edu/~rjhala/blast.html

http://www.splint.org

http://spinroot.com/uno/

http://cppcheck.sourceforge.net/#features

https://en.wikipedia.org/wiki/Sparse

https://cpachecker.sosy-lab.org

Even there it depends. 'Programming practices' is vague. Even C can be tamed, at great expense, using formal methods techniques. [0][1][2][3] Adoption of such methods can give a solid assurance of the lack of UB, like use of a safe language. Weaker measures, like adopting MISRA C, don't provide such strong assurances (although they can eliminate certain categories of errors), and as you indicate, their real value is a bit more subjective. Mandating a bad programming style could actively make things worse.

[0] https://trust-in-soft.com/

[1] https://www.eschertech.com/products/perfect_developer.php

[2] https://github.com/microsoft/Armada

[3] https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/