Programming Language Semantics and Memory Safety
13 points by abhin4v
13 points by abhin4v
Excellent post! The axiomatic view of UB was new to me! Though, my usual quibble applies: memory safety is a property of the implementation, and not of the language itself. Semantics getting “stuck” is not a problem per se, the implementation could safely halt in this case.
By your classification, can programming languages have any nontrivial semantic properties at all, or is all semantics part of the "implementation"?
Roughly speaking, a semantics describes the transitions (in an operational semantics) or reductions (in a denotational semantics) that are permitted, and you’d expect the permitted steps to describe something nontrivially useful.
The question is what happens when there isn’t a step specified in the semantics: does the implementation detect the situation and stop with an error, or blunder on? Or did the compiler prove that this kind of situation can never occur?
Back when I was learning this stuff in the 1990s, the typical aim when writing a formal semantics for a programming language was to demonstrate that a program could not get into a situation at run time where there were no valid steps (other than explicit cases like an uncaught exception). This was summarized by Robin Milner’s slogan, “well-typed programs cannot go wrong”. Which of course uses an excessively technical meaning of “go wrong” and even now 48 years later programmers are still arguing at cross purposes over whether not going wrong means having defined semantics or not being buggy.
Matklad mentions this at the end of his post, but there are some views of memory safety (e.g. The meaning of memory safety or The downgrading semantics of memory safety) that define memory safety as a (proper) hyperproperty, i.e. a property that can not be refuted by a single execution trace (finite or infinite) of a program. From this point of view, memory safety is about more than what happens when there isn’t a permitted step in the semantics.
FWIW, I "disagree" pretty strongly with the first paper. As in, the property they define is very interesting and useful. It's just unrelated to the thing we call "memory safety" in the industry. As a litmus test, JavaScript doesn't poss the property they define, while I consider JS to the the single industrial language which is memory safe with no strings attached (everything else, from Rust to Python, can be poked through with malicious code).
This is a bit of an ill-formed question: semantic properties live in the world of the abstract machine of the language, implementation generally concerns a specific concrete machine. You can't replace properties of one world with properties of another.
Regarding semantic properties, sure, there exist non trivial properties of the semantics itself (progress & preservation, "any program terminates", determinism), as well as semantic properties concerning specific programs ("this particular program terminates with zero input").
Does this help? Or am I misunderstanding your question?
I’m a bit confused on why can’t you? For example, suppose there is a language where you can only express programs that terminate otherwise it won’t type check and compile. Is termination not a guarantee of any concrete implementation expressible in this language or am I misunderstanding?
Great article but I have to quibble with one assertion:
When grown-ups talk about safety, they really mean cybersecurity
This is domain-dependent. If your codebase is firmware for a toaster oven, cybersecurity is a non-issue (unless your oven has networking for some stupid reason.) If it’s a word processor, security is a big deal only in limited areas like reading files (unless you stupidly have an overly powerful macro language.)
I’m presently rewriting a codebase in a safe language, primarily for reasons of development time and support costs. We spend too much time chasing weird bugs in the QE cycle and dealing with hard-to-diagnose customer issues. Many of these bugs are memory and/or thread safety problems.
I'm left scratching my head at what I missed in the article (which I read in its entirety) that qualified it as "great" and (matklad) "excellent". The examples seemed poor and obvious, and the conclusions seemed similarly poor and obvious. Maybe my expectations were just way too high? The only thing I learned was that he or she worked at Google, and I learned that several times over.
The topic is one that I am interested in. This article didn't do it for me.