My trouble with separate categories "memory safety technology" and "sandboxing technology" is that something like WASM execution is both:
* Depending on how WASM is used, one gets safety guarantees. For example, memory is not executable.
* Privileges are reduced as a WASM module interacts with the environment through the WASM runtime and the embedder
Now, when one compiles C to WASM one may well compile things with bugs. A memory access bug in C is still a memory access bug, but its consequences can be limited in WASM execution. Whether fail-stop behavior is guaranteed actually depends on the code the C compiler generates and the runtime (allocation/deallocation, concurrency) it sets up.
So when we enumerate immediately available security options and count WASM as sandboxing, this is not wrong. But WASM being an execution environment, one could do a lot of things, including a way of compiling and executing C that panics when a memory access bug is encountered.
Say your C program has sensitive information in module A and a memory safety bug in module B. Running that program in wasm won’t prevent the attacker from using the bug in B to get read/write access to the data in A.
In practice what the attacker will really do is use the memory safety bug to achieve weird execution: even without control over the program counter, the fact that a memory safety bug inside the wasm memory gives read write access to all of that memory means the attacker can make the program do whatever they want, subject to the wasm sandbox limits (ie whatever the host allows the wasm guest to do).
Basically wasm amounts to a lightweight and portable replacement for running native code in a sufficiently sandboxed process
Your general point stands - wasm's original goal was mainly sandboxing - but
1. Wasm does provide some amount of memory safety even to compiled C code. For example, the call stack is entirely protected. Also, indirect calls are type-checked, etc.
2. Wasm can provide memory safety if you compile to WasmGC. But, you can't really compile C to that, of course...
Correct me if I'm wrong, but with LLVM on Wasm, I think casting a function pointer to the wrong type will result in you calling some totally unrelated function of the correct type? That sounds like the opposite of safety to me.
I agree about the call stack, and don't know about GC.
That is incorrect about function pointers: The VM does check that you are calling the right function type, and it will trap if the type does not match.
Here it is in the spec:
> The call_indirect instruction calls a function indirectly through an operand indexing into a table that is denoted by a table index and must have type funcref. Since it may contain functions of heterogeneous type, the callee is dynamically checked against the function type indexed by the instruction’s second immediate, and the call is aborted with a trap if it does not match.
(Other sandboxing approaches, including related ones like asm.js, do other things, some closer to what you mentioned. But wasm has strict checking here.)
Depends on how it is used is already a sign that WebAssembly isn't really as safe as being sold, by many of its advocates, versus other bytecode formats.
Like, C is actually really safe, it only depends on how it is being used.
People only have to enumerate the various ways and tools to write safe code in C.
WASM is just a bytecode format for a stack based vm. Granted it is weirdly named, the actual "Assembly" equivalent is WAT.
But the point is, it is a format specification, which has nothing to do with safety. You can implement a totally unsafe WASM runtime if you so choose. Personally I think it's not a bad thing, at least we have something like it that can run in a browser environment. But I am curious to know why you dislike it so much.
> including a way of compiling and executing C that panics when a memory access bug is encountered.
WASM couldn’t do that because it doesn’t have a sense of the C memory model nor know what is and isn’t safe - that information has long been lost. That kind of protection is precisely what Fil-C is doing.
WASM is memory safe in that you can’t escape the runtime. It’s not memory safe in that you can escape escape the program running within the sandbox, which you can’t do with a memory safe language like Rust or Fil-C.
I remember a Luca Cardelli paper that explores a language with "type:type" and it contains a sentence roughly expressing: "even if the type system is not satisfying as a logic, it offers interesting possibilities for programming"
Small nit: As someone curious about a definition of memory safety, I had come across Michael Hicks' post. He does not use the list of errors as definition, and argues that such a definition is lacking rigor and he is right. He says;
> Ideally, the fact that these errors are ruled out by memory safety is a consequence of its definition, rather than the substance of it. What is the idea that unifies these errors?
He then offers a technical definition (model) involving pointers that come with capability of accessing memory (as if carrying the bounds), which seems like one way to be precise about it.
I have come to the conclusion that language safety is about avoiding untrapped errors, also known as "undefined behavior". This is not at all new, it just seems to have been forgotten or was never widely known somehow. If interested, find the argument here https://burakemir.ch/post/memory-safety-the-missing-def/
What's important is the context in which the term is used today: it's specifically about security and software vulnerabilities, not about a broader notion of correctness and program reliability. Attempts to push past that have the effect of declaring languages like Java and Python memory-unsafe, which is not a defensible claim.
This is a false dichotomy. Language design choices are the causes of security and software vulnerabilites. It is possible to recognize the value of GC languages and have precise technical terminology at the same time. We can invent new words.
I believe everyone who cares about memory safety appreciates that certain bugs cannot occur in Java and go, and if the world calls that memory safe, that is ok.
There are hard, well-defined guarantees that a language and implementation must make, and a space of trade-offs. We need language and recognition for the ability to push the boundary of hard, well-defined guarantees further. That, too, is memory safety and it will be crucial for moving the needle beyond what can be achieved with C and C++.
No one has a problem with applications being ported from low-level to GC-ed languages, the challenge is the ones where this is not possible. We need to talk about memory safety in this specific context, and mitigations and hardening will not solve the entire problem, only pieces of it.
The urgent problem is the problem settings where GC'd languages are not a good fit, including kernels and userland-kernels (AKA browsers). The problem is not that GC'd languages are insufficiently memory-safe.
Finally a good use case for decentralized technology? From https://www.eid.admin.ch/en/technology
"The e-ID architecture is based on a decentralised identity model that gives users full control over their identity and personal data. There is no central authority that aggregates, stores or controls credentials. Data flows occur directly and in a decentralised manner between the holder and an issuer or verifier. Linkability of usage across different services is technically restricted. Interactions between different actors also cannot be directly linked. During a verification process, the holder shares only the necessary data directly with a verifier, without the issuer being informed."
The verifier is the entity you hand your information to for verification, ie the CA. The extent of your interaction and linkage with them is mainly at point of verification and issuance.
It is however possible to trace a certificate to it's issuer, which on the surface sounds like a bad thing, but is in fact good if the goal is to provide privacy while ensuring accountability.
I mean in this case there is only one issuer, the Swiss state, so is that really a big deal? Ultimately the government is and should be the provider of identity.
Depends on the credential being issued. For the digital identity document it is the federal state, but the cantons (states) or even corporations are able to issue their own credentials using their own register.
Very interesting, that sounds a whole lot better than I envisaged. In theory your drivers license, passport, social number can all remain separate (not that it's necessarily set up like that in Switzerland). Thanks.
The privacy story of this looks better than the Norwegian BankID approach.
I would like if Norway moves in this direction, and I think that through the ongoing alignment with the EU wide program on digital id, that might happen.
I will quote (approximately) Simon Peyton Jones: "writing programs is not hard. Specifying what a program should do is hard."
Prove what? The author is well versed in the problem of specifications as the aliens-demand-gcc-correctness-or-else post. I also enjoyed the other post where they say "no one cares about correctness" and "people care about compliance".
It is safe to say, most people are not experts and will never become experts.
Being proficient in the business of coming up with suitable specification that can be implemented and getting assurance that an implementation meets the spec will most likely need all the kind of formal training for humans that the AI hype industry assures us is no longer necessary.
So it doesn't much help that LLMs are good at manipulating the tokens when used by experts, at least not in a big way. It can be hoped that they change cost-benefit balance in good ways, but the bigger problems of the industry will simply persist.
What would need to change for a more fundamental shift is getting a lot more people to understand the value of specifications. This is an education problem and paradoxically I could see AI helping a lot... if only there was enough interest in using AI to help humans become experts.
This change is happening as we speak. My work repo is now sprouting with markdowns primarily intended for agentic consumption, but it’s all dense jargon communicating requirements and important design decisions in a way which is useful to me as a software engineer. The toil of writing these specs from low level code is much lower today, because LLMs also help with that immensely.
In my workplace happens this, but in a bad way. There's a push to make use of AI as much as we can to "boost productivity", and the one thing people don't want to do is write documentation. So what ends up happening is that we end up with a bunch of AI documentation that other AIs consume but humans have a harder time following because of the volume of fluff and AI-isms. Shitty documentation still exists and can be worse than before...
Other than humans getting apoplectic at the word "delve" and — emdashes, can you explain and give some examples or say more about how AI-isms hurt readability?
Having encountered this spread across our orgs greenfield codebases which made heavy use of AI in the last 90 days: Restating the same information in slightly different formats, with slightly different levels of detail in several places, in a way that is unnecessary. Like a "get up and running quickly" guide in the documentation which has far more detail than the section it's supposed to be summarizing. Jarringly inconsistent ways of providing information within a given section (a list of endpoints and their purposes, followed by a table of other endpoints, followed by another list of endpoints). Unnecessary bulleted lists all over the places which could read more clearly as single sentences or a short paragraph. Disembodied documentation files nested in the repos that restate the contents of the README, but in a slightly different format/voice. Thousands of single line code comments that just restate what is already clear to the reader if they just read the line it's commenting on. That's before getting into any code quality issues themselves.
I've noticed AI generated docs frequently contain bulleted or numbered lists of trivialities, like file names - AI loves describing "architecture" by listing files with a 5 word summary of what they do which is probably not much more informative than the file name. Superficially it looks like it might be useful, but it doesn't contribute any actually useful context and has very low information density.
A piece of information, or the answer to a question, could exist in the documentation but is not in a format that's easily readable to humans. You ask the AI to add certain information, and it responds with "I already added it". But the AI doesn't "read" documents the way humans read.
For instance, say you need urgent actions from other teams. To this effect you order an AI to write a document and you give it information. The AI produces a document following it's own standard document format with the characteristic AI fluff. But this won't work well, because upon seeing the urgent call for action the teams will rush to understand what they need to do, and they will be greeted by a corporate-pr-sounding document that does not address their urgent needs first and foremost.
Yes, you could tell the AI how to make the document little by little... but at that point you might as well write it manually.
There is a place for informal, prose specs, and I can easily agree that more people are nowadays describing their programs in English.
The context here is formal specs though - adequately and precisely capturing the intended meaning (semantics) in a way that lends itself to formal verification.
Interactive theorem proving is interactive because proof search is intractable; a human articulates the property they want to prove and then performs the "search". Apart from the difficulties of getting to that proof, it can also happen that all goes through and you realize that the property is not exactly what you wanted.
I think you're missing a more internecine debate within software correctness/formal methods circles than the more general one about "writing good/correct software". Deductive theorem proving was all the rage in the 1970s, to the point that prominent people (Tony Hoare, Dijkstra) believed that it's the only way to write correct software. Over the years, the focus has shifted to other methods [1], from model-checking to unsound methods such as concolic testing and even property-based testing and code reviews, which have proven more effective than the deductive proof proponents had envisioned (Tony Hoare admitted his mistake in the nineties).
The problem with deductive proofs is that it's all-or-nothing, i.e. either you prove the theorem or you don't, and it's much harder to turn a knob to trade off cost for confidence and vice-versa than with other methods. Consequently, theorem proving has not benefitted from automation as much as it's alternatives, and is now viewed as having a too low bang-for-the-buck. But if LLMs can help automate deductive theorem proving, maybe that particular approach, which has gradually become less popular within formal methods circles but still has its fans, could make a comeback.
Of coure, specification is equally important in all methods, but the particular method of theorem proving has been disadvantaged compared to other formal and semi-formal methods, and I think that's what the author wishes could change.
[1]: Deductive theorem proving may be more prominent on HN than other formal methods, but as with most things, HN is more representative of things that spark people's imagination than of things that work well. I'm not counting that as a strike against HN, but it's something to be aware of. HN is more Vogue/GQ than the Times, i.e. it's more news about what people wish they were doing than what they're actually doing.
> The problem with deductive proofs is that it's all-or-nothing, i.e. either you prove the theorem or you don't, and it's much harder to turn a knob to trade off cost for confidence and vice-versa than with other methods.
This is not really true though. Sound type checking is a kind of deductive proof, but it's practically usable because it establishes very simple properties and is generally "local", i.e. it follows the same structure as program syntax.
Well, that's true for simple type systems. Dependent types are not so practically usable. You're absolutely right that simple types prove some "simple" properties, but we know what characterises them: they're inductive (or composable) invariants, i.e. P(a ∘ b) ⇔ P(a) ∧ P(b), for some program composition operator ∘ (I'm papering over some important but nuanced details). It's just that most program correctness properties we're interested in are not inductive, so the "proving power" of simple types is not strong (another way of describing it is that it's not powerful enough to express propositions with interleaved universal and existential quantifiers).
So when we talk about formal methods, we're usually interested in those that can express and/or "verify" (to some degree of confidence), non-composable properties and propositions that involve interleaved quantifiers.
>writing programs is not hard. Specifying what a program should do is hard.
But these two things are kinda the same thing. Writing a program is mostly just specifying what it should do in a very specific, unambiguous way. That’s why we have programming languages and don’t use English.
A PRD, a design doc and the code itself are kind of all the same thing, but with increasing levels of specification.
If you’ve ever played with formal specifications at some point you probably had the realization “wait a minute, I’m just writing another implementation of the program!” and in a way you are.
Spoken language descriptions of how to do something are incredibly underdetermined. Many people are likely familiar with the meme of following exact instructions on making a PB&J where a phrase like “put a knife in your hand and spread the peanut butter” can result in stabbing yourself and rubbing peanut butter on the wound. More than half of my job is helping other people know or otherwise determining what they really want a program to do in the first place.
"The program should accept one parameter as a number, and output this number multiplied by two" is a spec.
input a
print a*2
is a program.
But: why do that? why multiply by two? what does two represent? what do the input and output mean in the real world? what part is likely to change in the near future? etc.
Wrting the program isn't harder than writing the spec. Analyzing the problem and coming up with solutions is the hard part.
(And yes, LLMs are getting better at this everyday, but I think they still have a very long way to go.)
There is an old definition of language safety which means "no untrapped execution errors". It is not the only way to define safety, but it is a good way that you can adapt to various kinds of x-safety, such as memory safety.
No. A phantom type is a type whose only use is to communicate a constraint on a type variable, without having a runtime value that corresponds to it.
Typestate is a bit closer: it communicates some property where an operation (typically a method invocation) changes the property and hence the typestate. But there isn't necessarily a mechanism that renders the value in the old typestate inaccessible. When there is, then this indeed requires some linearity/affinity ("consuming the object"), but typestate is something built "on top".
The paper "Linearity and Uniqueness: an entente cordiale" by Marshall,Vollmer,Orchard offers a good discussion and explanation of the "opposite convention" you describe.
There is a dual nature of linearity and uniqueness, and it only arises when there are expressions that are not linear/not unique. At the same time, they have a lot in common, so we do not have a situation that warrants separate names. It is even possible to combine both in the same type system, as the authors demonstrate.
Taken from the paper:
"Linearity and uniqueness behave dually with respect to composition,
but identically with respect to structural rules, i.e., their internal plumbing."
A definition of memory safety without data race freedom may be more precise but arguably less complete.
It is correct that data races in a garbage collected language are difficult to turn into exploits.
The problem is that data races in C and C++ do in fact get combined with other memory safety bugs into exploits.
A definition from first principles is still missing, but imagine it takes the form of "all memory access is free from UB". Then whether the pointer is in-bounds, or whether no thread is concurrently mutating the location seem to be quite similar constraints.
Rust does give ways to control concurrency, eg via expressing exclusive access through &mut reference. So there is also precedent that the same mechanisms can be used to ensure validity of reference (not dangling) as well as absence of concurrent access.
> The problem is that data races in C and C++ do in fact get combined with other memory safety bugs into exploits.
Because C and C++ are not memory safe.
> A definition from first principles is still missing, but imagine it takes the form of "all memory access is free from UB". Then whether the pointer is in-bounds, or whether no thread is concurrently mutating the location seem to be quite similar constraints.
I think it's useful to work backwards from the languages that security folks say are "memory safe", since what they're really saying is, "I cannot use the attacks I'm familiar with against programs written in these languages".
Based on that, saying "no UB" isn't enough, and only looking at memory accesses isn't enough.
WebAssembly has no UB, but pointers defined to just be integers (i.e. the UB-free structured assembly semantics of a C programmer's dreams). So, attackers can do OOB and UAF data attacks within the wasm memory. The only thing attackers cannot do is control the instruction pointer or escape the wasm memory (unless the wasm embedder has a weak sandbox policy, in which case they can do both). Overall, I think that memory-safety-in-the-sense-of-wasm isn't really memory safety at all. It's too exploitable.
To be memory safe like the "MSLs" that security folks speak of, you also need to consider stuff like function calls. Depending on the language, you might have to look at other stuff, too.
I think that what security folks consider "memory safe" is the combination of these things:
1) Absence of UB. Every outcome is well defined.
2) Pointers (or whatever pointer-like construct your language has) can only be used to access whatever allocation the originated from (i.e. pointers carry capabilities).
And it's important that these get "strongly" combined; i.e. there is no operation in the language that could be used to break a pointer's capability enforcement.
Java and Fil-C both have a strong combination of (1) and (2).
But, long story short, it's true that a definition of memory safety from first principles is missing in the sense that the field hasn't settled on a consensus for what the definition should be. It's controversial because you could argue that under my definition, Rust isn't memory safe (you can get to UB in Rust). And, you could argue that wasm meets (2) because "the allocation" is just "all of memory". I'm not even sure I like my own definition. At some point you have to say more words about what an allocation is.
* Depending on how WASM is used, one gets safety guarantees. For example, memory is not executable.
* Privileges are reduced as a WASM module interacts with the environment through the WASM runtime and the embedder
Now, when one compiles C to WASM one may well compile things with bugs. A memory access bug in C is still a memory access bug, but its consequences can be limited in WASM execution. Whether fail-stop behavior is guaranteed actually depends on the code the C compiler generates and the runtime (allocation/deallocation, concurrency) it sets up.
So when we enumerate immediately available security options and count WASM as sandboxing, this is not wrong. But WASM being an execution environment, one could do a lot of things, including a way of compiling and executing C that panics when a memory access bug is encountered.