Reading for 11/30: CompCert

[zachary-kent]

Hello! @stephenverderame, @alifarahbakhsh, and I will be leading a discussion about the CompCert paper on 11/30. Please discuss your questions and insights below! Here are a couple questions to get started.

• The authors posit that completeness of the translation (for deterministic programs) does not need to be formally verified, and can validated through testing. Although soundness is undoubtedly more important, do you agree with this sentiment?
• Do you think verifying compilers for higher-level languages is tractable? The authors note that their backend is "lightly optimizing," yet still produces competitive code. Compilers for higher-level languages require more aggressive optimizations to generate good code--optimizations that would undoubtedly be difficult to verify.
• Is Coq the right tool for the job here? Do you think other interactive theorem provers (or approaches to verification) would be more effective?
• Do you see any obstacles to widespread adoption of CompCert for security-critical applications? As far as I know, many players in domains like defense *shudder* and avionics have built out their own proprietary compilers.
• The paper discusses how many translations that are taken to be obviously correct in compilers literature are significantly difficult to verify. Getting "lost in the weeds" is something I have too often experienced while developing verified software. How do you think we can minimize time and effort verifying code that is well-trusted?

[rcplane]

Speaking to safety critical aeronautic code verification, SpaceX uses Astree static analysis and extensive testing of its C++ flight control code base. As noted in a 2014 NASA example collection of formal verification methods applied to certification of critical systems, the onus of checking the model checker (and serious liability consequences) can lead to failure to share real full methods and case studies so each organization must resort to build and roll their own proprietary verification infrastructure. Also of note is that despite providing 203 pages of case study and supporting material, even they "do not address the verification of Executable
Object Code (Table FM.A-6 objectives), nor do we address the replacement of coverage testing by formal analysis" (pg. 16).
When management and auditors will want to see hardware operational testing for many scenarios including diverse conditions and long hours seeing a system running before certification, the additional effort complexity of formal verification is often judged prohibitive.

[stephenverderame]

This is a good point. For a while, CompCert itself was closed-source, and even today it still requires licensing to use commercially. A lot of the verification infrastructure is hard to develop, and many companies don't just want to give it away to their competitors.

I don't think formal methods will fully replace testing in the near future. A verified compiler can show that semantics are preserved during the transformation to assembly, but it can't show that the compiled code won't trigger some issue in the actual HW. In the US, the aim is for total object code test coverage on the real HW for this very purpose.

[ryanwmao]

Regarding the first question, while soundness indeed holds greater importance in compiler verification, dismissing the need for formal verification of completeness, especially for deterministic programs, might overlook potential risks. Overlooking completeness, even in deterministic scenarios, could lead to unnoticed discrepancies between the source and generated code that may evade testing. The paper's authors acknowledge that completeness issues are challenging to test comprehensively due to the vast input space, leaving potential corner cases unexplored; this could raise concerns about relying solely on testing to validate completeness, as testing might not cover all possible scenarios, potentially leaving critical vulnerabilities unaddressed. While soundness takes precedence, considering formal verification for completeness ensures a more comprehensive assurance of a compiler's correctness, minimizing the likelihood of undetected issues in compiled code.

[sampsyo]

Could you explain a little more about what you mean by this?

Overlooking completeness, even in deterministic scenarios, could lead to unnoticed discrepancies between the source and generated code that may evade testing.

If I understand the context of this line of discussion correctly, "completeness" here just means "does the compiler actually terminate and generate some code for all valid programs, instead of giving up with an error?" So by that interpretation, an incomplete compiler still does not generate bugs ("discrepancies between the source and generated code"). Maybe I'm missing the point here?

[he-andy]

One major obstacle to the widespread adoption of CompCert in sectors like defense and avionics is the established reliance on proprietary compilers. These industries often have stringent requirements for security, reliability, and compatibility, leading them to develop or use custom-tailored compilers. Shifting to an open tool like CompCert might raise concerns over control, integration with existing systems, and meeting specific compliance standards. Additionally, the transition would require significant investment in terms of training, testing, and possibly modifying the tool to fit into established workflows. These factors combined make the adoption of CompCert a challenging proposition for industries that rely heavily on proven, bespoke software solutions.

[xalbt]

I agree that the adoption CompCert into existing systems, particularly in security-critical applications like embedded systems, would be very challenging. Through some initial research, I discovered that many of these applications, including NASA's Curiosity rover which uses the VxWorks operating system by Wind River, often rely on custom compilers. Other defense projects use proprietary compilers from GreenHills Software. The realm of real-time operating systems and embedded systems demands specialized functionalities from compilers, distinct from what standard compilers offer. This specialization likely involves considerable engineering efforts, making these compilers uniquely suited to their specific applications. Therefore, bridging the gap between CompCert and these specialized compilers will be at least overcoming the technical differences and efforts already invested by makers of the proprietary software and also the additional factors mentioned by Andy. However, I don't believe this gap is insurmountable. It's possible that entities like GreenHills and Wind River could gradually incorporate techniques or parts from CompCert, especially for verifying the most critical aspects of their systems.

[bennyrubin]

Besides the question of CompCert being used "in the wild" and integrated into real security and mission critical applications, I think it has a ton of value as an open source research project. I always think it's a shame when instead of working together, companies or government agencies all independently work on the same problems, without sharing any insights with the rest of the community. Whats nice about CompCert is that anybody, from the academic community or from industry or defense, etc. can build on the ideas to make their compilers correct and more secure.

[sampsyo]

This general point about the context of verified compilation is important and under-appreciated, IMO. It is one reason why we need both approaches to exist: "clean-slate" verified compilers like CompCert and "lightweight" verification tools for existing infrastructures, such as the Alive paper we read a few weeks ago.

[obhalerao]

Just because code is well-trusted does not necessarily mean it is correct; indeed, this paper was able to find bugs in many trusted C compilers (CompCert included). If we truly want a fully verified compiler, then it is important to ensure that all parts of the compiler in question are verified. Though CompCert does come a long way in terms of verifying certain aspects of compiler correctness, it's important to note that there can always still be lurking bugs in its unverified components.

[zachary-kent]

Yeah -- we had a similar discussion about Alive earlier in the semester. I don't think it's productive to view verification as "all or nothing," and even then CompCert is closer to "all" than it is to "nothing". I'd also add that bugs in the parser are probably much easier to diagnose than subtler ones introduced by unsound optimizations.

[jdroob]

The paper you referenced looks like it came out in 2011 and the CompCert paper appears to have been published in July 2009. I'm wondering if some of the CompCert bugs found were related to the parts of the compiler that were not yet verified when the CompCert paper was released in 2009 (i.e. the parser, the assembler, the linker). I do think that proving semantic preservation from the source program down to the compiled program should be a goal, with the understanding that compiler bugs may still pop up. But after reading this paper, do I think verifying compilers is tractable for high-level languages? Maybe? Honestly - not sure though.

The semantics of Clight is formally defined in big-step operational style. The semantics is deterministic and makes precise a number of behaviors left unspecified or undefined in the ISO C standard.

I know C is somewhat notorious for having unspecified or undefined behaviors, but could this still potentially pose a problem when attempting to verify a compiler for a modern, high-level language?

[sampsyo]

While I unfortunately don't have a reference about this on hand, it is certainly true that the TCB for CompCert has shrunk (i.e., more stuff has been verified) since then! Perhaps as a response to efforts like Csmith that have found bugs in the unverified parts of the toolchain.

[stephenverderame]

This is a great point. What is verified on CompCert's end has grown quite a lot, and we plan to bring up CSmith and the more recent developments of CompCert during the discussion today.

[SanjitBasker]

I think that there's still some value added by verifying a single part of a compiler--for instance, register allocation can take a while to get exactly right, and more efficient algorithms have a lot of moving parts. I think that in this case, the implementation could serve as a good reference for others who are implementing the same algorithm and want to make sure that they're not missing any edge cases.

[matth2k]

Do you think verifying compilers for higher-level languages is tractable?

I guess not.

The added value of CompCert lies not in the compilation technology implemented, but in the fact that each of the source, intermediate and target languages has formally defined semantics, and that each of the transformation and optimization passes is proved to preserve semantics in the sense of section 2.4

Formal verification is not magic, so it doesn't seem like their methods would scale well to more complicated programming languages, architectures, or optimization strategies. It sounds like too much work. For example, wouldn't a lot of the perks of object-oriented programming, like dynamic polymorphism, be hard to reconcile with formal verification?

Are semantics often the bottleneck of formal verification methods? I'm not very familiar with the research area, so I am curious what you guys think.

[zachary-kent]

I think the largest barrier is just the massive amount of work required to write proofs, mechanized or not. The pool of compiler engineers is already quite small, and the subset with experience in verification is even smaller. Many research projects are successful because they're limited in scope, but CompCert (and verified compilers) are not; these are large-scale engineering projects, requiring an appropriately sized team.

Also, Coq can just be unpleasant to use, sometimes producing really bad error messages with inaccurate sources. Its tactic language, Ltac, is also a bit obtuse and is currently being replaced with something a bit more ergonomic. Hopefully these issues will be addressed as the language matures.

[bcarlet]

On the issue of supporting higher-level languages, I wonder how much demand there is for a fully verified compiler that also supports complex language features. High-assurance software often adheres to guidelines that limit use of an already simple language like C to even simpler subsets thereof; it's not clear to me that supporting compilation of features like runtime polymorphism would make sense within this domain. After all, having a verified compiler doesn't help with the verification of the software itself, and using those features makes that more difficult as well.

[stephenverderame]

C definitely has a good foothold, but there is a reasonable interest in higher-level languages for safety-critical SW. I know of at least one company writing aviation SW in (a subset of) C++17. And in the US, there is an entire supplement to the guidelines for certified aviation SW development that's dedicated to object-oriented programming (DO-332).

[yxd97]

I think there might be an approach where you only change a bit of the code in each compliation step, similar to MLIR. Composing proofs for little changes may make this problem practical, but the question is how many steps do we need to lower a high-level language to machine code.

[sampsyo]

I can't help but comment on this specifically:

For example, wouldn't a lot of the perks of object-oriented programming, like dynamic polymorphism, be hard to reconcile with formal verification?

We actually have a recent paper about adding support for Rust's OO-like dynamic dispatch functionality in a formal verifier! This one's a bounded model checker instead of a certified compiler toolchain, but it's something:
https://www.cs.cornell.edu/~avh/dyn-trait-icse-seip-2022-preprint.pdf

[keikun555]

Reading the line,

Despite intensive testing, bugs in compilers do occur, causing the compilers to crash at compile-time or—much worse—to silently generate an incorrect executable for a correct source program.

reminded me of Ken Thompson's Turing award lecture on introducing silent vulnerabilities (or even exploits) into the C compiler: https://www.cs.cmu.edu/~rdriley/487/papers/Thompson_1984_ReflectionsonTrustingTrust.pdf

I hope that verified compilers will give at least some more confidence that our compilers are secure.

[bennyrubin]

That is a really good point I had not thought of. Besides ensuring correctness, being able to see a proof of soundness for a compiler translation also gives assurance that the code can be trusted, as long as you can verify the specification is correct. I believe one of the takeaways of Ken Thompson's lecture was that you cannot trust anything you didn't write yourself, but formal verification gives another avenue to obtaining trusted code. In fact, just having a verifier should be enough.

[sampsyo]

I highly recommend the "trusting trust" paper (it's short!) as added bonus reading! It's a worrisome and eye-opening experience, and I won't spoil the ending.

[willwng]

Do you think verifying compilers for higher-level languages is tractable? The authors note that their backend is "lightly optimizing," yet still produces competitive code. Compilers for higher-level languages require more aggressive optimizations to generate good code--optimizations that would undoubtedly be difficult to verify.

This does feel like the end-goal, to have a language that is inherently safe(r than C) with a verified compiler. Maybe this is wishful thinking, but looking at the benchmarks I want to say this will come sooner than later. The use of "verified verifier" is also interesting; the optimizations can be more easily implemented and then a verifier comes along and checks afterward. There are tradeoffs with complete correctness but it seems certainly possible to handle the aggressive optimizations in most use cases

[willwng]

I'm also curious if CompCert's multiple intermediate languages are standalone; compiling to these seems like one could get verification for free

[zachary-kent]

They are! A research compiler I personally worked on targeted Clight.

[vivianyyd]

I know an attempt to verify LLVM is in the works. It'd be neat if we could have verified MLIR. I wonder if such a thing is reasonably doable

[sampsyo]

This is mostly just a hot take and not carefully substantiated, but: there is a problem here that is a kind of "magnified" version of the economic problem with implementing any compiler where language popularity/practicality is self-reinforcing. That is, it's more economically rational (but perhaps disappointing) to invest more in existing/legacy compilers for extremely popular languages (because they affect more code) than to make new languages and new compilers that would be fundamentally better.

I say formal verification is a "magnified" version of this principle solely because it involves even more effort! If humanity can really only support one effort like CompCert, then I think it makes sense to do it for C, where the code for air traffic control systems and radiation dosage devices already lives. But it's also kinda sad, because of course we would abstractly prefer if these things were written in a language with a higher baseline level of correctness.

[emwangs]

This paper was the first time that I had seen things from my System Security class outside of the class, which was super fun! Terms like trust, high-assurance, low-assurance -- security terms with heavy implications -- really brought me to the realization that frequently we do have a lot of axiomatic trust in our compiler stack. Writing correct source code is hard enough, and frequently developers have the mindset of "the compiler is going to help optimize something like this, because the compiler is smarter than me." Looking at this -- and how we can only verify a very small subset of C (even though they say its a large subset, they make a lot of C's flexible memory manipulation impossible) -- does not provide a very strong basis for trust in our compilers at all. I know that software engineers are meant to mitigate this by doing a lot of testing and good code writing, but many software developers also do not do those things, and makes we wonder if it's a bit disheartening that we must have some large number of vulnerabilities hiding in source code around the world due to compiler bugs? Or if most vulnerabilities still come from source code, rather than compilation.

Side note, I like how the semantic preservation definition is predicated on "S safe" -- its a bit remniscient on like... C++ compilers having an incredibly long list of undefined behaviors that say "because you have this UB, your program can go absolutely wild now." I wonder if that is exactly done for semantic preservation and "S safe"?

[sampsyo]

I think it's a very good question to ask how many bugs in the real world are due to compiler bugs! It's obviously an incredibly hard question to answer (because there is fundamentally no way to get a census of real-world bugs). But if you want to get a little bit scared about the possibility, here is a cool paper about security vulnerabilities that are caused by compiler bugs:
https://www.usenix.org/system/files/usenixsecurity23-xu-jianhao.pdf

Here's another systematic study about how much the bugs found by compiler fuzzing arise in practice:
https://dl.acm.org/doi/abs/10.1145/3360581

[stephenverderame]

Side note, I like how the semantic preservation definition is predicated on "S safe" -- its a bit remniscient on like... C++ compilers having an incredibly long list of undefined behaviors that say "because you have this UB, your program can go absolutely wild now." I wonder if that is exactly done for semantic preservation and "S safe"?

This is exactly what they do. CompCert can only prevent the introduction of bugs from the compiler, and can't protect your code from itself.

[collinzrj]

The main advantage of this unconventional approach, compared with implementing the compiler in a conventional imperative language, is that we do not need a program logic (such as Hoare logic) to connect the compiler’s code with its logical specifications.

This is really interesting. I'm very curious about how exactly the code of the compiler itself and the proof of algorithms are bridged. This argument seems to imply that functional languages are easier to prove then conventional imperative language. Why is this the case?

[sampsyo]

Extremely broadly, this (functional languages make proofs easier) is true simply because of the lack of side effects. Imperative languages can make semantic modeling really tricky because you have to assume that any expression might affect any other through hidden state. In a purely functional language, every expression's meaning only depends on its inputs.

Of course, adding higher-order programming (functions as values), which is another common ingredient in what people mean by "functional languages," makes things more complicated again…