FYI you may want to take a look at the effort going on to start standardizing similar features for C and C++ (P1315 for C++, soon for C too). If this paper goes through, we may get some "secure clear" primitive/built-in in LLVM which we may be able to take advantage from rustc too, both for explicit clearing (e.g. zeroize) as well as stack clearing by the compiler.
In addition, there have been some research efforts on ways to implement stack clearing in some compilers which may worth taking a look at. For instance, see the SECURE project for GCC referenced in the paper .
Within Rust, there is also the secstr crate referenced in the paper, in case it hasn't been mentioned.
I am happy to see more efforts in the same direction! I will reference the zeroize and secrecy crates in the next revision of the paper.
An approach for the wording would be to lift the provision in [intro.abstract]p1 (i.e. the “as-if” rule) for calls to this function; thus conforming implementations need to emulate the behavior of the abstract machine and therefore produce code equivalent to having called the function, even if it has no effect on the observable behavior of the program. This is the same approach C11 takes for memset_s :
Unlike memset , any call to the memset_s function shall be evaluated strictly according to the rules of the abstract machine as described in (126.96.36.199). That is, any call to the memset_s function shall assume that the memory indicated by s and n may be accessible in the future and thus must contain the values indicated by c .
It's not clear to me what this means and how this could be specified operationally.
Why would we (necessarily) need to specify it operationally to begin with?
We can keep deferring this problem to users, but the reality is that they need a solution. Otherwise, bugs end up cropping up in real projects as the paper shows.
Therefore, I argue there has to be a way to guarantee a clear of a memory region in a systems programming language that is not rendered void by some transformation.
I would agree with that if we were not talking about Rust, i.e. how is Rust a "high-level general-purpose language"? It certainly deals with low-level details and systems programming, and even the book, the nomicon and the reference acknowledge this.
Don't get me wrong, I know you are a language team member, but I am genuinely surprised about such a characterization.
What ends up happening otherwise in practice, if we go for an axiomatic approach is that the implementation becomes the spec, and there is really nothing (at least not a formal mathematical definition) to judge its correctness against, because you may have mutually incompatible stated properties.
I don't think Rust needs to solve every problem, especially those that cannot be well-specified. It seems more appropriate to provide a solution at the level where guarantees can actually be made (and not just claimed to be made).
I also don't see what's specific to systems programming in the use case here. Why would it e.g. not apply to Haskell but apply to Rust? Moreover, I do not find arguments of the form "A is a systems language, A has X feature. B is a systems language, so therefore it must also have X" persuasive. Ideas need to stand on their own merits, not on whether e.g. C or C++ also do something.
Which is not a problem in practice. Rust is a counter-example on its own, given that it does not have (or hasn't had, if that is not true anymore) a formal spec; and yet that does not stop us from using it.
Those claiming that languages need a formal specification covering every single corner (rather than an informal one, or even no specification at all) are the ones that have to prove such a level of formality is needed. Note that having such a formal specification is, of course, great, but please don't let that get in the way of engineering.
I think most people would agree that Rust current main goal is to be a better, safer replacement for C and C++, i.e. a better alternative for systems programming. Given that a subset of systems programming projects need to solve this problem (e.g. Linux, OpenSSL), then it would be ideal that Rust provides a solution.
Rust (and C, and C++) compilers can very much provide this guarantee. A particular abstract model may not, but that is a problem of the spec or the chosen model being unsatisfactory. Again, as I said in the first point above, that is not a bad thing: coming up with those models is hard.
I only said systems programming languages need a solution for that problem. Whether non-systems languages require a solution or not is another (interesting) discussion.
That is not the argument I presented, though.
The motivation presented in my paper is pretty much irrelevant of whether we are discussing Rust, C or C++. In fact, I am going to send a similar RFC for Rust with pretty much the same content.
What that article argues about is controversial and many experts in the field definitely do not agree on trying to mold languages like C into "high-level" languages without regard for well-established semantics . The reason is simple: C was born and is still used for actual low-level systems programming, and some of those changes and new characterizations are effectively backwards-incompatible with already written code years back. In the process, they have introduced bugs, more work for engineers and, in the worst case, security issues .
Or, picking this from another angle: if we were to call C, C++ and Rust "high-level general-purpose", then the moniker would not be very useful as there would be no "low-level general-purpose" languages around, at least those common and/or intended for usage by humans.
I was discussing "high-level general-purpose". Rust isn't a DSL, of course.
I'd very much like to have such a guarantee. But this is a hard problem, and it doesn't go away by saying "there must be a solution".
Not caring about the (complex and subtle) operational behavior of languages such as C, C++, Rust and LLVM-IR is how we ended up with bugs like this or this: without a precise definition of what exactly the observable behavior is that has to be preserved according to the "as-if" rule (what we call "[contextual] refinement" in academia), we are doomed to use a flawed intuition and end up with sets of optimizations that all seem to make sense in isolation, but are just plain wrong when combined.
Doing so is the only technique that I know of that can hope to prevent the kind of bugs I cited above. I'm open to other solutions to this problem, but I don't know any.
Doing "just engineering" is what got us where we are: all major compilers have serious bugs in their optimizations that stem from fundamental misunderstandings about the actual semantics of the language they are implementing. The bugs I cited in my previous response were all related to pointer provenance, and similar bugs are present in ICC and MSVC (based on statements of some of my coauthors on this paper). I doubt pointer provenance is the only such case, it is just the biggest one we found so far.
The fact that all major compilers have the same kind of bug shows that this is not the usual bug where someone made a small mistake in implementing a particular optimization; this is systematic. Something about how these compilers are developed is fundamentally flawed. I believe the flaw is in not having a proper idea for what the actual semantics are of the language that is being optimized, using a flawed mix of "what the C spec says" and "what the hardware does" instead. I think this is a proof that some "level of formality is needed".
We should prevent such issues from arising again. The only technique that I know to ensure this is to take an operational view, to equip the IR on which the optimization happens with a precise operational semantics with a notion of "observable events" and argue that the optimizations do not change the observable behavior. This requires making explicit many things that are usually left implicit, like the fact that memory in these languages doesn't just store plain bytes.
Note that we do not necessarily have to make this fully formal and mathematically tight. Having, for example, a reference interpreter for a language (one that adequately models not just the "good case" but also all possible causes of UB), would probably be sufficient. Something like Miri -- though Miri does not currently explicitly model what is observable and what is not.
I am not entirely sure what your argument here is. Your sources all give good reasons for why C maybe shouldn't be a high-level language, but that doesn't change the fact that these days, it is (at least the variant of C implemented by compilers such as gcc and clang), and applying low-level reasoning leads to logical contradictions.
There is a fundamental trade-off for a language: either it is low-level or is is aggressively optimized. Todays C/C++ are the latter, and does does Rust. Any way we can find to break this trade-off is welcome, but it should be a proper solution, not hand-waving.
As a case in point, when it comes to union semantics (one of the issues raised in your sources), I stronlgy argued for giving Rust the simplest possible semantics I can imagine, allowing all forms of type punning and whatnot, precisely because of how bad an idea the C rules turned out to be. Due to this, Rust does not have a notion of an "active field" of a union, or other surprising forms of "hidden state". Being explicit, operational, formal and high-level doesn't contradict taking into account low-level concerns. But not being explicit, operational and formal is how C and C++ got where they are: the language semantics are so unclear that informed and intelligent people can argue for hours about their details. I strongly think that we can do better than that in Rust, but we'll have to adjust the methodology to achieve that.
As I said before: this is a hard problem, it doesn't go away by pretending it doesn't exist.
Agreed, but the actual problem (users implementing some solution for that) does not go away either. And we end up with projects being wrong and unsafe, and sometimes not known until months have passed because the compiler didn't expose it.
Some of those bugs are created by standards and compilers trying to be too smart and introducing that complex and subtle behavior that nobody asked for to begin with. We all want powerful transformations, but we should not let that get in the way of making (unsafe) code almost impossible to reason about with confidence. While Rust can attack this problem nowadays in a much better position, the way it was done over the years for C and C++ was definitely wrong since it broke existing projects.
What about not implementing a model or optimizations that are not in line with what people use the compiler for? Note that I say this as someone that thinks Rust can get away with a lot more than C/C++ in this, because it is a "new" language (in the sense that there is not decades of code around that were written with other expectations of behavior).
I am not a compiler writer/researcher so I cannot really address the rest of your quote. However, what you wrote in this sentence is precisely what I asked about in a reply above. Yes, having a hole in the model is bad, and it may lead to bugs in the compiler and its passes at some point or another. However, those dealing with that (compiler writers) are way more capable to solve it than users of the compiler, and they can solve it centrally for all their users.
Those sources are arguing to go back to the previous behavior, for good reason. The fact that some compilers implement a broken language (for a particular purpose) does not mean C is high-level either. In fact, as you very well know, GCC and Clang have had to backtrack on some of their decisions and/or add compiler switches so that they didn't break existing code.
So, what is "C"? Whatever a compiler team thinks it should be based on some reading of the standard today, or what the users and their millions of LOC have been using it for, for decades? Should we ignore all existing code just because it allows us to implement a fancy transformation? Should we demand engineering all over the world to change their code?
An example is Linux, as I mentioned in the reference, but it is not by any means alone. I have worked in some projects where optimizations were completely disabled because "legacy" code was not going to be replaced/rewritten at all and very expensive equipment depended on it. Yes, we can come today and say that it was "broken code" according to the standard or the newer compilers' reading of it, but the fact is that code like that exists everywhere.
Note that I don't really care whether C is one thing or the other. But I do care compilers and standards bodies changing the semantics. I am all for enabling new behaviors and opportunities in new C/C++ standards (and I enjoy them in some projects!), but please do not say the new standards are (all of) C/C++ (even if ISO tells us they are :).
[In any case, I think this is a bit off-topic and quite controversial]
I acknowledge it is a hard problem, but similarly, we can say: pretending Linux, OpenSSH and other major projects are not facing the ("actual") problem does not go make it go away, either.
Note that in my discussions on this topic with the C++ committee, some experts agree with your assessment and its difficulty, but many (including compiler writers) also agree that the problem should be solved by the standard anyway, one way or another (i.e. even if a formal approach cannot be found right away, the standard should provide the means to users to deal with the issue).
Here's a simple, high level overview over where I think the disconnect between you and @RalfJung is.
Compilers have two main jobs: compile code to get the correct result, and compile code to get the correct result quickly.
The former is more or less specified by the language specification, however it exists, in a somewhat formal definition or just by the behavior of existing compiler(s).
The latter is achieved by applying optimizations to the generated code/IR. This is made reasonably possible exclusively by "dead space" in language semantics: the "undefined behavior.
It is impossible to add new (meaningful) optimizations without exploiting this dead space. This means that any new optimization (or bug fix!) will lead to code that existed on the old compiler giving a different result. (At the very very minimum, timing is different, and that is technically observable.)
Though it may not be your position, it comes off as if you're effectively advocating for any change in the result of a compiled program to be disallowed. This is because giving the compiler to the entire world to work with is basically isomorphic to every possible program being written. This argument simplifies down to no more optimizations, permenently, because it will break someone.
There's a reason that there aren't any (good?) raw assembly optimizes: it's downright impossible to optimize "what the machine does" programmatically. Any higher level language (here: has some abstraction layer between it and the hardware) adds extra rules (and thus, undefined behavior for breaking those rules). That dead space is exactly what allows optimizations to work.
Your argument is basically that the formalization effort needs to consider practical uses and lend itself towards comprehensibility. Nobody disagrees with you there. In any language that exposes a way to write something that is UB, it should be as simple as possible for the author (with the help of static tooling) to avoid causing UB.
At this point I'm going in circles, so I'm not going to go off the point of this thread any further.
But the key point of this is that a feature like this which is intrinsically dependent on the actual hardware (as it sits exclusively within the designed dead space of the language) is not and cannot be specified/guaranteed by the language specification. At maximum, it can be promised by a specific implementation/backend to fulfil specific hardware-level goals.
Optimizations don't break code, they make logical inferences based off of UB impossibilities that make sense locally to transform code to be quicker. This breaks when the author does not come in with the same exact assumptions. And not even all optimizations are solely modelable as source transformations.