Spectre and the end of langsec | Hacker News Reader

Spectre and the end of langsec

wingolog.org

264 pointsrobin_reala190 comments

I'm starting to consider whether this reflects a larger failure in the industry/community: Traditionally, many of us (I'd say almost all) have been focused on security at the OS level and above. We've assumed that the processor and related hardware are safe and reliable.

However, below the OS level much new technology has been introduced that has greatly increased the attack surface, from processor performance enhancements such as branch prediction to subsystems such as Intel ME. I almost feel like Intel broke a social compact that their products would be predictable, safe commodities on which I can build my systems. But did those good old days ever really exist?. And of course, Intel naturally doesn't want their products to be commodities, which likely is why they introduced these new features.

Focusing on OS and application security may be living in a fantasy world, one I hesitate to give up because the reality is much more complex. What good are OpenBSD's or Chrome's security efforts, for example, if the processor on which they run is insecure and if there are insecure out-of-band management subsystems? Why does an attacker need to worry about the OS?

(Part of the answer is that securing the application and OS makes attacks more expensive; at least we can reduce drive-by JavaScript exploits. But now the OS and application are a smaller part of the security puzzle, and not at all sufficient.)

The issue of hardware security really has been ignored too long in favor of the quest for performance enhancement. Perhaps there is a chance now for markets to encourage production of simplified processors and instruction sets that are designed with the same philosophy as OpenBSD. I would imagine companies and governments around the globe should have developed a new interest in secure IT systems with news about major exploits turning up every few months now it seems.

It reflects the industries priorities: performance and productivity. That's all. You can make the argument that these priorities are wrong, but we've known such attacks were theoretically possible since the vulnerability was introduced.

Even now I'm certain there are many companies not even bothering to patch against Spectre and Meltdown because they've deemed the performance degradation to be worse than the risk, and that's a perfectly rational decision to make.

I'd heard Jon Callas of PGP talking about concerns over hardware-level security -- CPU and baseboard systems / BMCs -- in the mid naughties. So this stuff has been on at least some peoples' radar. Not particularly widespread, perhaps.

Theo de Raat turned up with a ~2005 post specifically calling out Intel as well, though not necessarily speculative execution that I'm aware.

Really not the end. The existence of issues that cannot be addressed via 'langsec' does not imply that we should give up on 'langsec'. There will be more security issues due to buffer overflows than there will be CPU bugs this year. More importantly, there will be orders of magnitudes more users with data compromised via buffer overflows, compared to CPU bugs.

The author does not seem to mean "the end of langsec" as in "everyone will give up on it", but rather the end of a period characterized, and not incorrectly, by the opinion that a safe programming language guarantees the absence of unintentional unsafe behaviour. In short, that things which, within this "langsec framework", one could prove to be impossible, turn out to be possible in practice; in the author's own words:

"The basis of language security is starting from a programming language with a well-defined, easy-to-understand semantics. From there you can prove (formally or informally) interesting security properties about particular programs. [..] But the Spectre and Meltdown attacks have seriously set back this endeavor. One manifestation of the Spectre vulnerability is that code running in a process can now read the entirety of its address space, bypassing invariants of the language in which it is written, even if it is written in a "safe" language. [...] Mathematically, in terms of the semantics of e.g. JavaScript, these attacks should not be possible. But practically, they work. "

This is not really news. The limits of formal methods were, in my opinion, well-understood, if often exaggerated by naysayers, brogrammers or simply programmers without much familiarity with them. Intuitively, it is not too difficult to grasp the idea that formal proofs are exactly as solid as the hardware which will run the program about which one is reasoning, and my impression is that it was well-grasped, if begrudgingly, by the community.

(This is akin to the well-known mantra that no end-to-end encryption scheme is invulnerable to someone looking over your shoulder and noting what keys you type; similarly, no software-only process isolation scheme is impervious to the hardware looking over its shoulder and "writing down" bytes someplace where everyone can access them)

Wait. Who has ever said this? We've had soundiness as a fundamental concept for years. I'm not aware of a single static analysis tool that is truly sound. Everything is always "sound with respect to X". The academics surely haven't been the ones making a claim that correct programs truly are immune to any and all problems. If we ended this period, we did it ten years ago.

> the end of a period characterized, and not incorrectly, by the opinion that a safe programming language guarantees...

I don't think that there was ever such a period. Provable correctness always had the caveat of highly idealized assumptions, and we've known from the start that hardware vulnerabilities such as timing attacks, rowhammer, gamma rays, and power loss can undermine those assumptions.

Well, how about a provably secure hardware description language then?

It's funny that you mention buffer overflows. An interesting thing to point out—and I'm not sure if anyone has; I've looked before—is that if you follow Meredith Patterson's line of reasoning about langsec for protocols in particular, you end up at the conclusion that C-style, NUL-terminated strings are the right way to do things.

This doesn't mean there aren't other defects in the apparatus where C exploits thrive. It's just that (if you adhere to the langsec school of thought) you are required to confront the conclusion that it's been pinned on the wrong thing.

Why are C style buffers any more correct than Pascal strings?

LangSec says that we should use the weakest model of computation that can get the job done. Patterson specifically recommends hewing to regular expressions as much as possible, but otherwise going no higher than deterministic context-free for ordinary programs.

Null-terminated strings can be recognized by a regular expression, but once you introduce a length field, you (theoretically) need at least a context-sensitive grammar, which is excessively powerful (read: difficult to reason about) for ordinary programs, according to LangSec.

Where theory and reality diverge, I choose to believe reality. A theory that says null-terminated strings are more secure than length-delimited ones is a theory that needs to be taken back to the shop and examined for why it is wrong.

I can imagine a much, much richer theory that might produce "in a perfect world that didn't have any other errors, null-terminated strings would be better". For instance, while this is far from the only problem with null-terminated strings, a lot of their badness historically came from the mistake of mixing stack string data with stack values that say where to return, or mixing the strings with places where you can also put executable code. In a world that had a different kind of stack, null-terminated strings would be less bad. But they would still be bad enough that length-delimited would still be better from a security point of view. And theories of security that are this sensitive to the mistakes around them aren't very useful in the real world, where mistakes will abound and useful security theories need to be able to degrade with some grace whenever possible.

That depends on what you mean by "getting the job done". If what you want is to write a reference description of a protocol for a paper, and make mathematical proofs of the protocol's properties, that's one thing. (The weakest model of computation there means you'll spend less proof effort around your surroundings -- language, environment -- and more on the protocol, giving you less leeway for error).

If you want to write a real-world implementation of the protocol, then the story is different, because the complexities of the real world are unavoidable. You will add complexity to your toolset, to deal with the aspects of the environment that you abstracted away in your paper.

When we write proofs for papers about type systems, we use ultra-simple languages like some typed variants of lambda calculus, which are the simplest thing that gets the job done. But once the type properties are proved, no one is expected to write their real programs that way -- they are expected to replicate those properties in the real world instead.

I suspect it's because they can't get out of sync in a way that causes OOB reads. You could have the null too early in the buffer but can't have it too late. With Pascal strings you could have a buffer of size 18 but with a length tag of 30 and have no way to know you're going overflow.

In terms of a buffer overflow, how would any of that make any difference ? If you somehow manage to overwrite the length prefix due to some shoddy pointer manipulation (and buffer writes) and, subsequently, write past the end of the string buffer, how is that different from just writing past the end of the string buffer in the first place ?

With Pascal strings, you at least have a fighting chance in terms of knowing the actual size of the buffer.

This is naïve first-order thinking; we can justify length-prefixed strings on a more abstract basis. First, note that in a trusted kernel, we'll prefer to define our string-handling functions only once and then explicitly hand-write their correctness proofs. This means that, on a higher level, we do not have to prefer any one particular string abstraction just because of the white-box implementation details; we'll call strcat() either way.

Now, note that we can store any character, including NUL, in a length-prefixed string. However, we cannot do this in NUL-terminated strings. This is because stray NULs will change the apparent length of the string. More directly, what a string is, whether it's "string of length 5" or "string of length 255", is determined by the string's data. In contrast, a length-prefixed string contains two fields, and only one of them controls the length of the string.

Now, imagine that an attacker comes to totally control the contents of our string. In the NUL-terminated scenario, they also control the length of the string! This does not occur with length-prefixed strings. There is strictly less capability offered to the attacker.

I know about the automaton-based approach to langsec, but this capability-based analysis is far more in line with the recent rise of weird machines.

> Rich Hickey has this thing where he talks about "simple versus easy". Both of them sound good but for him, only "simple" is good whereas "easy" is bad.

I don't think I've ever heard anyone mischaracterize his talk [1] this badly.

The claim is actually that simplicity is a fundamental property of software, whereas ease of use is often dominated by the familiarity a user has with a particular set of tools.

[1] https://www.infoq.com/presentations/Simple-Made-Easy

Agreed, but I have see a lot of people come away from the talk with an unfortunate disdain for ease. Ironically, in disentangling "simple" and "easy", Rich created a lot of confusion about the value of ease.

My personal take is that perhaps chipmakers will start to see different market pressures. Performance is the big one, and it's been around since the first microprocessor. Power became increasingly more important, particularly in the past decade, from both ends of the market. (Both mobile devices and supercomputers are very power conscious.)

Security may become a new market pressure. You will likely sacrifice performance to get it, as it will mean simpler cores, maybe in-order, and probably without speculative execution. But, with simpler cores, we can probably further increase hardware parallelism, which will only partially mitigate the loss in single-threaded performance. Some chips may even be more radically security conscious, and guarantee no shared caches between processes. Such chipmakers would be able to say: we can't say for certain that these chips are fully secure, but because they are simpler with less attack vectors, we are far more confident they are. Security conscious chips may tend to be the ones that are internet facing (your mobile device, cloud data centers), and faster, less security conscious chips may only exist behind strict firewalls.

I bring this up in response to the submitted article because I find it unlikely that we will start to model processor insecurity at the language level. It ruptures too many levels of abstraction. I find it more likely that we will find ways to maintain those abstractions.

I'm less familiar with Spectre than Meltdown but part of the issue to me seemed to be that everything hinged on the principal of memory isolation. To the point where all of physical memory was mapped from the kernel which was mapped to the user address space. It felt to me like having 1 great big lock and assuming it couldn't be broken.

I get that when you make the assumption that you cannot depend on memory isolation a lot goes out the window, but could there be a more layered approach that lessens the damage done when some assumption like that is challenged or is it appropriate to wait until that time to make changes?

The amount of damage possible when that assumption is chosen to be false seems to warrant considering changing the way process memory is mapped. This is at a software level but its similar to what you were saying, when is speed and performance going to be sacrificed for preemptive security measures? I'm sure that it already is in some ways since all security has a performance hit, but allocating processes and virtual memory is such a core feature of the kernel that I can imagine the performance hit could be significant (or was it just laziness to map all of physical memory to the kernel address space?)

> Security may become a new market pressure. You will likely sacrifice performance to get it, as it will mean simpler cores, maybe in-order, and probably without speculative execution.

Maybe we go from having CPU + GPU to having CPU + GPU + FPU, where FPU = "Fast Processing Unit".

The CPU in the CPU/GPU/FPU model becomes simpler. Any time we have to choose between performance and security we choose security.

The FPU goes the other way. It is for things where speed is critical and you either don't care if others on the machine can see your data, or you are willing to jump through a few hoops in your code to protect your secrets.

For most of what most people do on their computers most of the time, performance is fine without speculative execution or branch prediction and probably even with caches that are completely flushed on every context switch. (It will probably be fine to leave branch prediction in but just reset the history on every context switch).

The FPU memory system could be designed so that there is a way to designate part of FPU memory as containing secrets. Data from that memory is automatically flushed from cache whenever there is a context switch.

I believe you can make a process noncacheable today, and maybe even disable branch prediction. This would totally shut down Spectre and Meltdown. You can disable SMT, and there's a whole host of other things you can do to isolate your "secure" process on an existing chip. Nobody has done these things because they like performance.

For most of what most people do on their computers most of the time, performance is fine without speculative execution or branch prediction

I think you underestimate the importance of branch prediction.

We already have that in ARM phone SoCs with big.LITTLE.

I think this is too dark a post, but it shows a useful shock: Computer Science likes to live in proximity to pure mathematics, but it lives between EE and mathematics. And neglecting the EE side is dangerous - which not only Spectre showed, but which should have been obvious at the latest when Rowhammer hit.

There's actual physics happening, and we need to be aware of it.

If you want to prove something about code, you probably have to prove microop semantics upward from verilog, otherwise you're proving on a possibly broken model of reality.

Second-order effects are complicated.

"There's actual physics happening, and we need to be aware of it." Yes, maybe abstractly. However, the Spectre flaw is well above the level of physics. There may be physics flaws as well (e.g., Rowhammer), but Spectre is an architectural flaw in the design of some microprocessors, in that it leaks information by e.g. cache timing attacks and non-program-state data (e.g., branch prediction tables). These can be redesigned above the physics layer.

I can't speak for the author of that quote, but cache timing appears to be as much a physics phenomenon as is the behavior that allows rowhammer to work. I cannot see any point where the author implied that the solution can only be found in the physics layer.

The cache timing is not a physics phenomenon. It's an isolation phenomenon. Speculative execution is loading data into the cache, exactly as designed. The instructions that used the speculatively loaded cached data were not retired, exactly as designed. Requesting that cached data later (in actually retired instructions) is faster assuming it's still cached, which is a reasonable likelihood given the locality of the access. That's the timing attack vector. There's no physics here - it's all architecturally operating as designed. That's why the design has a security flaw, and there is no physics problem here. (There may be others, elsewhere, of course, but none in Spectre or Meltdown that I am aware of.)

From my POV "the locality of the access" making a speed difference is a physics phenomenon.

The fact that is working as designed has no bearing on the question of whether it is a physics problem. You could just as well say (as Intel's press release seemed to to be trying to imply) that there isn't a fault at all, whether physical or not, because it is working as designed.

But your own description of it working as designed is within the context of a state-machine model, and in that model, there is no attack vector; that only appears when you take the physics of the implementation into account. There wouldn't even be a cache except for the temporal physics of memory access. That it works as designed is beside the point because the design did not take the physics into account.

Looking at it from the other direction, how do you conclude that rowhammer does exploit a physical phenomenon, without being inconsistent about what that means?

This is a bit of a nitpick, but when you say Computer Science I think you mean Software Engineering and/or Computer Engineering. These are very different fields, and Computer Science is by-and-large agnostic of any actual physics.

As an anecdote: my Computer Science PhD dissertation contained all of about 12 lines of pseudocode, and these are only to provide a more direct description of an idea than I was able to provide with several paragraphs of prose. Hardware / architecture / physics is entirely irrelevant to it -- while any implementation of the ideas therein should be aware of hardware / physics / etc., we are solidly entering the realm of engineering at that point.

Rowhammer I can understand, but how do you come to that conclusion--"neglecting the EE side is dangerous"--from analyzing Spectre? Does speculative execution rely somehow on physical effects? I can't find anything ( for example here: https://en.wikipedia.org/wiki/Spectre_(security_vulnerabilit... ) that suggests there is a physical component to this vulnerability.

I'd argue that using timing differences due to physical limitations of the hardware that to exfiltrate data based on whether or not it's cached is very definitely 'relying on physical effects'

> timing differences due to physical limitations of the hardware

I see; so you're talking about step two as described here, do I have that right?

https://en.wikipedia.org/wiki/Spectre_(security_vulnerabilit...

This seems like a failure of algorithm design to me, in the sense of not starting with a better model that more accurately encodes the possibility of timing attacks. That being the case it appears to me to be a problem still firmly residing in the domain of computer science.

But, I'm a programmer, not a chip designer, and I have very little knowledge of this field, so I'm probably biased and not thinking about this correctly or with enough nuance.

Quoting the thread root:

> Computer Science likes to live in proximity to pure mathematics, but it lives between EE and mathematics

which doesn't disagree with "firmly residing in the domain of computer science" - it's merely a question of nobody having factored the right bit of EE into the right bit of math to get the right model.

>There's actual physics happening, and we need to be aware of it.

More specifically, we're not running software on physics, software is physics - CPUs are simply physical structures designed in such a way as to be extremely easily mathematically modeled. Software is nothing more than runtime configuration of hardware.

> If you want to prove something about code, you probably have to prove microop semantics upward from verilog

What if your chip fab doesn't obey the HDL's instructions?

You're always "trusting trust" at some level. See also this horror story: https://www.teamten.com/lawrence/writings/coding-machines/.

> The "abstractions" we manipulate are not, in point of fact, abstract. They are backed by real pieces of code, running on real machines, consuming real energy, and taking up real space. [...] What is possible is to temporarily set aside concern for some (or even all) of the laws of physics.

– Gregor Kiczales, 1992

I don't see how this is fundamentally different than timing attacks and other side channel attacks that have been well known before, and to the best of my knowledge, simply hasn't been the focus of the "prove it correct" approach.

Whenever you want to prove something correct, you need to make assumptions about the execution model, and about what correctness means. Now "we" as an industry found a bug that makes the actual model differ from the assumed model, so we need to fix it.

The same is true when you can measure the power used by a microchip during some cryptographic operation, and infer the secret key from that -- even if the cryptographic operation has been proven correct, the definition of correctness likely didn't include this factor.

While langsec can't easily mitigate spectre because the processor is trying to hide where the performance comes from, it's worth noting that several new languages are working on ways to write code where you can actually assert and have the compiler check that the timing of the code you write is bounded and uniform.

It's very easy, I think, to throw up our hands and say, "Well gosh all this language stuff is useless because timing attacks are so scary!" But in reality, they're pretty well studied and many of them are actually pretty simple to understand even if they can be hard to recognize.

Both hardware AND software sides of our industry need to start taking correctness, both at compile and runtime, seriously. The days where we can shrug and say, "But that's too slow, don't run code you don't trust" are dead. We killed them by ceding the idea of hardware ownership to big CSPs. The days where we can say, "This is too complicated to do!" or "This doesn't deliver customer value!" are also going away; the threat of combination attacks easily overshadows any individual attack, and small vulnerabilities tend to multiply the total surface area into truly cataclysmic proportions.

But also gone is the day when we can say things like, "Just use Haskell or OCaml!" We've seen now what these environments offer. It's a great start and it's paved the way for a lot of important understanding, but even that is insufficient. Our next generation of programming environments needs to require less abstract category theory, needs to deliver more performant code, and needs to PROVE properties of code to the limit of runtime resolution. The hardware and OS sides of the equation need to do the same thing. And we as engineers need to learn these tools and their techniques inside and out; and we shouldn't be allowed to sell our work to the general public if we don't.

> several new languages are working on ways to write code where you can actually assert and have the compiler check that the timing of the code you write is bounded and uniform.

I'm interested in how that would avoid the halting problem. Let's say I write code, compile it, and run some "timing verifier" on it. That verifier either runs my code and verifies that it's timing is correct on that run, or inspects the machine code against a known specification of the hardware I'm running it on right then and ensures all of the instructions obey my timing constraints. How would you check that the code's timing is bounded and uniform on subsequent executions? Or on other hardware? Or in the face of specifications that are incorrect regarding the timing characteristics of machine code instructions (CPU/assembly language specs are notoriously incomplete and errata-filled).

I suspect something fundamental would have to be changed about computer design (e.g. a "CPU, report thine own circuit design in a guaranteed-accurate way") to make something like this possible, but am not sure what that would be, or if it's feasible.

It avoids the halting problem the same way literally all sound static analysis does. With false positives. The java type checker will reject programs that will not have type errors at runtime. And a system that verifies timing assertions with SMT or whatever will reject some programs that will not fail the assertion.

The halting problem has never actually stopped static analysis tools. Static analysis tools that check timing assertions have been around for a very long time.

Sure, but this isn't a static analysis tool in the same way a type system is. This is an analysis tool which checks for mostly platform-unrelated, entirely runtime behavior which can vary based on a lot of external factors.

When you say "Static analysis tools that check timing assertions have been around for a very long time.", what are you referring to? I've used analyzers that check for potentially-inescapable loops, do assembly/machine code operation counts, and look for the presence of interruptions that are known to take a potentially infinite/nondeterministic amount of time (waiting for I/O), or ones whose lower bound in time is known (scheduler interactions like sleep). How would you analyze for instructions which have theoretically-constant times, but which in practice are vulnerable to "constant plus or minus"-type timing attacks like Spectre? How would that analysis yield results we don't already know, a la "in this section of code, you should obfuscate/prevent the gathering of timing data, and/or try to defeat speculative execution"?

There is no one here saying that there is a runtime that can protect against Spectre. Spectre is just one of extreme example of timing attacks which have been troubling our industry for the better part of a decade.

It's entirely possible to prove that some types of code do not significantly very they're running time based on the character of their input. A classic example of this is hashing algorithm whose execution time is only dependent on the length of the input.

I'm not sure if people recall password oracles but they're still valid attacks today. We can only eliminate these by starting at the bottom and working our way up.

If your response to Spectre is to give up on your computer security, I don't think I want you writing software for me. These are the challenges our industry has to face. Failure is not really an option.

The Halting problem as a burden for this kind of code analysis is very overstated. What you do is instruct the compiler how to infer timing inductively on a language of all basic internal and I/O ops.

And of course it's 2018, nothing stops us from saying "Your software needs training." We can go from a somewhat conservative binding that is then informed by runtime metrics to be very precise for a given deployment and as long as we hold the system static for that measurement, it's pretty fair.

As for Hardware verification, I agree it's a harder problem in some ways, but since there is no obfuscation of the important timing quantities it also gets easier.

Everyone is assuming the author is giving up on Langsec. Read carefully, he called Spectre/Meltdown a setback. I think he’s making a subtler point that the fundamentals of programming have become more of a pragmatic activity than a mathematical one, if you’re being practical about your goals that is. I’m currently on the kubernetes multi-tenancy working group (which isn’t really a working group yet) and its really funny to see how much effort is going into securing containers, but core bits like the CNI receive little attention. A wise security professional, ex hacker said that he actually liked over engineered security systems as a hacker, because it told him what not to focus on. Container security pretty good? Okay then figure out how to do what you want without breaking out of the container (definitely possible in the case of Spectre/Meltdown).

There is a fundamental cognitive bias in our field to solve the technically challenging problems without realizing that there are practical vulnerabilities that are far more dangerous, but a lot more boring to solve (the most common way orgs are exploited is through a combination of social attacks and something really trivial).

I think the author is frustrated because he feels the interesting work is unimportant in comparison to the practical.

That isn’t to say that this work isn’t helpful. I’m very glad to be working daily in a typesafe, memory safe language, but I have bigger fish to fry now as a security professional on the frontline.

On the one hand, langsec specifically handles these problems. A program for searching through a file will produce the same results whether it runs in a tenth of a second or ten seconds, and as such doesn't need to - in langsec, shouldn't be able to - access the time. That's what langsec is. It can even identify hazards like the SharedArrayBuffer high-res timers that compare the execution speed of different programs by communicating between processes; most programs shouldn't care which thread finished first, so that information shouldn't be available! And so we build formalisms for computing that don't make that information available to the program.

On the other hand, that's probably infeasible for the real world. Humans care about time too much for it to be declared off-limits to many programs. Similarly with things like communicating processes. These attacks are so fundamental that it'd be effectively impossible to build a program that didn't throw up an impenetrable wall of critical langsec violations.

So I'm not sure. The langsec framework does offer a solution. It might just be that, in the same way that things like haskell offer their solutions, it's too difficult for the real world to apply it.

There are CPUs that are immune to these attacks, including spectre.

The CERT recommendation was to throw away affected CPUs and use alternatives.

Now this isn't very realistic today when the in-order alternatives are slow and not comparable performance. But it does say that CERT is not giving up on langsec.

(Team Mill - we're immune too and will put out a light paper on how these attacks apply to in-order processors that support speculation and what we're doing to prevent them)

> Team Mill - we're immune too and will put out a light paper on how these attacks apply to in-order processors that support speculation and what we're doing to prevent them

Will this be sent to the mailing list when released?

Yes probably.

I've already written the paper and it's just got to survive a lot of peer review. It turns out that it would be real easy to envisage an in-order processor that has some mechanism for speculation that was actually vulnerable to spectre and variations of meltdown and the paper explores that - so hopefully it's an interesting paper even if the tl;dr is we claim to be immune.

I'm curious, because I think the Mill as described in the talks is vulnerable to a variant of Spectre. If you have a sequence of code like this:

    if (index < bounds) {
        index2 = array1[index];
        ... array2[index2];
    }

If the compiler speculates both array accesses above the bounds check, then the first one can still succeed (i.e. not produce a NaR) while accessing attacker-controlled memory for the value of index2.

You could obviously fix this by never generating code that does double speculation, but you could also do that by modifying a conventional OoO microarchitecture.

Spot on!

This variant of Spectre would be software bug not a hardware bug on the mill.

Our specialiser had to be fixed to not produce code with this flaw.

And so we wrote a light paper on it, and perhaps a talk etc ;)

It seems that Mill's combination of a single address space and speculation-before-permissions-checks is still quite vulnerable to an ASLR leak. Have you made any changes to mitigate this, or do you just consider address space layout leaks acceptable behavior?

seriously? Mill is/will do speculation before perms? And here I thought turfs were the elegant answer to this nightmare.

See slide 72 of the metadata talk[1] and slide 51 of the IPC talk[2], which indicate that it does speculation before permissions checking.

Since turf permissions operate on the granularity of an arbitrary address range (rather than a page like traditional MMUs), the permissions cache (what the Mill calls a PLB) has a worse latency/power tradeoff than a traditional TLB. The Mill takes advantage of its single address space and reduces some of this hit by doing permissions checks in parallel with the access.

[1] https://millcomputing.com/docs/metadata/ [2] https://millcomputing.com/docs/inter-process-communication/

Thank you for watching the talks! :D

Luckily its not quite as you interpreted:

The L1$D is accessed in parallel with the PLB. Both at top-level caches - one for data, one for protection.

If there is a PLB miss we have no cache-visible side-effects until the protection has been resolved.

The paper we're preparing will cover this in detail, because as you can see, the talks are a bit light on exactly what happens in what order when here.

>Our specialiser had to be fixed to not produce code with this flaw.

Isn't prefetching/load-hoisting pretty much required to get any sort of performance out of an in-order VLIW-like machine?

Been checking the Mill forums manually waiting for a detailed post from yourself or Ivan about the matter.

For reference, there is an interesting thread from someone who seems like they knew the nature of the issue before the disclosure, to which Ivan replies discussing some of the complications of implementing branch prediction [0]. Ivan concludes with:

> "To answer your final question: no, branch prediction is not actually necessary, and Mill uses exit prediction instead. But so long as memory latency is much longer than a compiler can see, and path fanout remains larger than hardware can handle in parallel, prediction of some kind will be necessary for performance."

This is interesting as many people are now debating just what types of speculative execution, if any, can actually be performed without exposing security risks.

[0] https://millcomputing.com/topic/prediction/#post-3049

One of the big problems with Spectre and Meltdown is that they are due to behaviours and components of a processor that are not well documented. Caches, branch predictors, out of order execution and superscalar execution are all things that processor vendors refuse to disclose any information about because it is so commercially sensitive. Indeed CPUs are now primarily differentiated by these features. We are no longer getting processors with faster clocks or even smaller transistors so a lot of research has gone into making individual instructions run faster (or at least run faster most of the time).

Neither Intel, ARM or AMD have disclosed why their CPU design are, or are not vulnerable to Spectre and Meltdown. If the developers of compilers or even operating systems don't know exactly how the hardware works then it is pretty hard for them to know that they haven't written vulnerable code. By the same token, it is also hard for them to know if they have written performant code.

And we know even less about other types of processors that exist in almost every chip such as GPUs, digital signal processors, video processor units (VPUs) and other hardware accelerators. Those processors can almost certainly also leak data from other parts of the system, they have their own caches and sometimes branch predictors. Although it is hard to specify the code that runs on these devices it is almost certainly still possible to exploit bugs and timing attacks in them.

We are essentially getting security through the obscurity of the devices and security through obscurity is no good.

So should we have processor architectures which are completely open? In some ways that would destroy most vendor's business models. But having more openness could lead to more divergent processor architectures as vendors try to differentiate themselves and it should improve the security of our systems.

Welcome to the cyberwar.

I think the basic problem with brakdown of static analysis tools like this one or optimisations like speculative execution is that they were built in a different time for significantly different requirements.

When the theories were developed, the main concern was to prove correctness and protect against accidents. Yes, the OS isolated processes from each other and protected memory boundaries - but this was added to keep a crashing process from corrupting other processes and bringing down the whole OS. It was not developed to contain an actively malicious process.

At some point the paradigm changed and the idea spread that an OS shouldn't just protect against misbehaving code but also against misbehaving programmers. That lead to the current practice of compartmentalizing a machine in different areas of trust and tightly restricting what a program can do - and at the same time permitting increasing amounts of "untrusted" code to run because we trust the boundaries so much.

I think the general paradigm shift has some worrying sides, but more importantly, it was never explicitely discussed and it was never discussed if the current tools of software and hardware development can even support that new paradigm.

So yeah, in short, I think we are currently discovering that our houses are in fact not built to withstand a 20kton TNT blast set off at the front door. So far this hadn't been a problem as random violent explosions used to be a rare occurence. Somehow we got ourselves in a situation where they aren't rare anymore.

Am I wrong in recalling that Itanium (IA-64) was an in-order architecture that relied on the compiler to explicate the potential for parallelism? Again, if I recall correctly, the struggle to construct compilers that could do this versus the apparent success (and lack of trade-offs) in letting in-processor circuitry to reshuffle instructions at run-time was one of the main reasons why x86’s 64-bit extensions prevailed (the other being poor performance when running legacy x86 32-bit code).

Now it turns out that we really were benefitting from an advantage that had a hidden cost, not in terms of performance (though power might be a concern) but in terms of breaking the implicit model we have of how software executes, and that this disconnect in turn opens us to a host of “architectural” risks and metaphor breakages.

Maybe at this point we should consider reverting to the original plan and insist on compilers doing the legwork, so that approaches such as langsec have a hope of succeeding. Systems must be comprehensible (at least in principle) and reliably deterministic from the top all the way to the bottom.

Itianium relies on advance loads which is a form of speculation introduced by the compiler to perform competitively. It is not unlikely that this is as exploitable as spectre.

I respectfully disagree for two main reasons. Firstly, because the compiler is not transversal to all processes currently executing on the system at runtime, so it isn’t a ”unifying step” that conjoins otherwise independent processes and can allow them to interact. Secondly, if the compiler were found to be leaking state between processes, simply changing the compiler’s logic would allow rectification of these issues (albeit at the expense of recompiling all software with the new compiler), with circuits etched onto a processor die one has no such opportunity. What could be (at least potentially) an open-source fix becomes the umpteenth binary blob from an opaque entity that tell us to ”trust them because [they] know best”.

Spectre is not (at least not directly), a cross address space vulnerability (although it can be exploited in some cases from other address spaces).

A JS JIT running on itanium that generates advanced loads before bounds checks will be vulnerable.

It is true that it can be fixed purely by software changes, by simply avoiding issuing advanced loads [1], but then again software changes can also plug the spectre v1 vulnerability on OoO architectures by adding artificial dependencies on load-load sequences (see the WebKit mitigation article that was discussed here a few days ago). Both software fixes have potentially significant performance issues (more so on in-order architectures).

So yeah, in-order CPUs are less microarchitecturally vulnerable [2] to spectre by default, but the compiler tricks required to make them competitive with OoO CPUs might reintroduce the issue.

[1] In principle compiler issued prefetches and load hoisting can be an issue on OoO CPUs as well, but as these are less important for performance compilers can be more conservative. On the other hand some VLIW architectures have special instructions and architectural support (like Itanium ALAT) to make this load hoisting easier.

[2] There are in-order ARM CPUs that have been reported to be affected though.

Thinking more about this, the vulnerability would be in any load issued speculatively which whose address depends on the result of a previous load. This can be detected at compile time and avoiding just this scenario it will not have such a performance effect as avoiding any speculative load.

Here's a more optimistic take which is unavoidably a plug.

Urbit is maybe a sort of "extreme langsec." "Immune" is a dangerous word. Urbit is "premitigated" against Spectre for the following reasons, some cool and others stupid:

(1) The Nock VM has no O(n) data structures, ie, arrays. This was not anything to brag about till now.

(2) Urbit events are interpreted in their own process, which is one trust domain (one process, one "personal server").

(3) A personal server isn't a browser and doesn't habitually run code its owner doesn't trust.

(4) Urbit is purely functional, so you only know the time if someone passes you the time.

(5) Top-level event handlers are passed the time of the event. This is easy to fuzz.

(6) If you are running untrusted foreign code, it is probably just a function. Giving this function a measured time interval from top-level event times would be strange. And it would need another channel to exfiltrate the stolen data.

Never say never, but this combination of premitigations makes me worry about Spectre very little. Although, when we do have a less-trusted tier of applications (walk before run), ain't nobody is going to be telling them the time.

Besides the plug, the lesson there is that one of the reasons Spectre is a problem is that langsec is an imperfect bandaid.

Urbit is premitigated because it was designed as a functional system from the ground up. The JS environment is functional lite -- it allows typeless functional programming, but it also retains many mutable/imperative systems design tropes.

It's these tropes that have become clever attack vectors. If you don't want to get Spectred, build systems that are formal and functional all the way down.

>(5) Top-level event handlers are passed the time of the event. This is easy to fuzz.

Therein lies the rub -- if your program does not have access to precise timing information, it is by definition not operating at the full capability of the hardware which runs it. That's a hard sell to many domains.

Consider gaming. At 144Hz w/ 4K resolution you have 6ms to render a frame: that's about 1.3ns per pixel. If for a moment we imagine that it takes approximately 1 machine cycle per pixel to render a scene: that means you need to be operating at 1.3GHz just to meet the deadline for drawing to the frame buffer. -- That's before you consider memory & cache latency, or the fact that your multitasking OS is stealing resources for itself & other competing processes.

So no, one cannot just fuzz performance counters in the name of security. Any soft-realtime or hard-realtime domain is going to expect the machine to actually perform as advertised.

You are right: by definition real-time tasks will always be vulnerable.

With regard to Urbit, it is a non-issue because there are no use cases which would warrant access to soft or hard-realtime for a networked OS.

Such tasks will always happen on client-side, by virtue of network latency.

> Spectre shows us that the building blocks provided to us by Intel, ARM, and all the rest are no longer "small parts understood entirely"; that instead now we have to do "basic science" on our CPUs and memory hierarchies to know what they do.

I object to the term "no longer" in that sentence. There exist old CPUs that are not vulnerable to these attacks, but their existence doesn't mean that when those CPUs were in widespread use they were "understood entirely". I imagine that most programmers affected by the F00F vulnerability in Pentiums didn't fully understood what it was about the chip/microcode that caused the lockup, either.

The parts being assembled change over time, but I think you can always say "bah, {kids|engineers|scientists|etc} nowadays don't know how the things they're plugging together work" and be trivially "correct" without making any constructive point about how to go back to some nonexistent past in which things were understood. Even when computers ran on vacuum tubes and physical insects in machines as "bugs" ([apocryphal](https://www.computerworld.com/article/2515435/app-developmen...), I know), people didn't know the composition of the hardware. Would one of those programmers, on average, be more likely to fully understand, say the heat range required for successfully making circuits in a tube or the effects of anode corrosion on the lifespan of a tube, than a modern-day program would understand how CPU microcode works?

The amount of complexity per part might go up over time. But there's always a specialized threshold for "low level" understanding below which a) most people don't operate and b) dragons lurk.

I find weird and worrying that you cannot analyze the safety of a program easily with some form of static analysis, or that there is no solution to do an automated security audit.

I have been bragging for a long time that there are no organized effort (state, government, scholars or otherwise) to teach basic software security in programming. There are no ISO standard for computer security, or at least there is nothing really relevant being taught. Security certifications don't really mean anything, or it seems nobody cares enough.

I guess governments will have to get preoccupied with those things, because you can clearly see that for now, it's an arms race kind of strategy, as long as the NSA has the upper hand, things are okay, but if it becomes a bigger national security concern, things might change. I guess you can smell that the russians are getting good enough and that it's time to make internet security a more prevalent matter for developers.

How can you hope to statically analyse something that executes non-deterministically and whose state depends on the goings-on of all the processes simultaneously hosted on that system? The whole point the author is making is that there is a step at the bottom of all formal reasoning hierarchies that doesn’t behave deterministically and thus undermines formal reasoning about everything built above it. It’s just that we had never recognised it as existing because we conveniently abstracted away this reordering of instructions and thus had a model of the runtime environment that doesn’t match with reality.

>Mathematically, in terms of the semantics of e.g. JavaScript, these attacks should not be possible. But practically, they work.

Obviously this is badly stated.

It's not correct to say "mathematically they should be possible given the semantics of Javascript" and then say that "practically they work" as if implying that the mathematics somehow broke down.

It's not the mathematics that failed you, but the assumptions (axioms) you've used. Mathematically they are absolutely possible -- when you correctly account for the real processor behavior. And if you had mathematically modeled the whole "JS semantics + CPU behavior" accounting for Meltdown, mathematics would have shown that it's not safe.

Spectre has nothing to do with program correctness or safety. It has everything to do with hardware's correctness and safety.

That is, the basic premise of hardware process isolation is that a process cannot have any knowledge of what another process is doing, or whether it even exists, unless it is explicitly permitted (e.g. the OS offers an API to look at processes).

This basic premise is now broken: enough information leaks via timing as to allow to read arbitrary memory regions. It's like you built a house laying bricks in a formally correct way, but the walls proved to be permeable because the bricks themselves have a flaw.

Since this flaw is not fundamental, that is, not even every currently existing processor exhibits it, it appears to be reasonable to replace the flawed design of the bricks, and not to re-engineer house construction.

There is a nice quote in the article, about doing basic science to find out how software (and hardware) actually works, since specs are badly incomplete. It can be matched with another, earlier famous quote: "Beware of this code; I only proved it correct, I did not test it." Black-box testing of information systems is not going anywhere, formal methods or not; at the very least, we need evidence that formal methods were not visibly mis-applied, and also evidence that other basic premises, like those of hardware, still hold. Because sometimes they don't.

> Since this flaw is not fundamental, that is, not even every currently existing processor exhibits it, it appears to be reasonable to replace the flawed design of the bricks, and not to re-engineer house construction.

Timing leaks are an absolutely fundamental flaw of computers. It may be the case that this specific instance of speculation-based attacks that leak information via timing channels can be fixed by stopping speculation or by complete rollback of speculated state including caches. "It's the chip's fault" is true for Spectre and Meltdown, yes, and it will take some time for Intel and other manufacturers to design new chips that stop leaking information due to speculation.

However, timing attacks are probably everywhere. They are covert channels that subvert language safety. The question isn't whether information leaks, but what and how fast. How are we going to deal with them comprehensively at the language level? I don't know.

Uh, there are literal piles of papers on static analysis of timing based confidentiality leaks. We've been studying this for years. It is a hard problem, but by no means new or insurmountable.

And there are literally billions of lines of code and billions of devices that have never been analyzed for timing leaks.

Industry reality is that we are still fighting stack overflow bugs 40 years after safe languages were invented.

Timing attacks are going to be around a long time.

Security did not appear a feature worth spending money on in many cases.

As devices become more powerful and more connected, thus increasing the attack surface and the potential losses form them being cracked, the cost-based analysis will start to prioritize security more.

The tools for writing dramatically less brittle code are there, but there's the cost of switching. It needs to become lower than the potential losses. And with the current state of the industry, the losses and lawsuits are surely coming. Remember what it took to make an average e-commerce website become reasonably secure.

It's going to take a LOT of money. Where does this money come from, or on what gets less money get spent, to use instead to pay the very significant cost of security we haven't been paying?

Do you mean buffer overflow? What language protects against stack overflow?

It's not languages but compilers that protect against stack overflow. Rust has contributed code to LLVM that causes stack overflows to abort the process (via guard pages and stack cookies), which means that theoretically you could enable this for C and C++ as well. See https://github.com/rust-lang/rust/issues/16012

If you forbid self-recursive functions, the required depth of stack can be statically analyzed. I believe such tools exist even for (a feature-limited subset of) C.

Not just self-recursion, but all recursion, including transitive mutual recursion. I think it may be possible to do this via strictly lexically-scoped symbols (so imagine C with no forward declarations). Might still be ways to sneak recursion in there though.

That's what fix point combinators are for. The Y combinator won't work in a language like C++, but the Z will work fine.

For example, here's Z in C++14, used to compute 5 factorial: https://godbolt.org/g/se5B8u

Yeah, I specifically had combinators in mind when considering ways to sneak recursion in. :P And it occurs to me you'd have to forbid function pointers too.

Yup, and you would probably not be able to do Object Oriented Programming either (or have to limit it horrendously), cause an object is similar to a closure, and you therefore can use it for unbounded recursion.

Yes, I meant any recursive calls via a chain of calls to other functions.

I think proving that no recursion exists should be relatively simple, just keep following the call graph and keep a set of the nodes (functions) called; you either reach the terminal node(s), or reach an already-visited node again, which means a recursion exists.

What if functions are first class? Then imagine a function gets passed in as an argument and called. You won't know what function you're calling until runtime.

I thought that self recursion was fine so long as the calls were provably "smaller problems" than the function calling them, something like "bounded recursion".

If you can prove that the recursion is bounded, great!

But sometimes it is hard, and I'm afraid it's equivalent to the halting problem in general case.

Without recursion, though, finding the maximal depth of the call graph is definitely solvable, and likely not even very hard.

Really? I thought the problems were equivalent, of proving that e.g. a loop vs its recursive equivalent were bounded.

Side note: an interesting case is the Stable Marriage Problem. It's easy to write the O(n) algorithm and prove its bound, but it's hard to translate into a bounded recursive algorithm that does the same thing.

(At least as far as I understand -- I searched it on Stack Overflow and that's what it said, and I've tried the problem itself. A Coq fanatic insisted that "if you can prove the run time is bounded it's easy to write the bounded recursive equivalent" but somehow that never translated into an actual insight on how to do it.)

Proving that a loop is bounded is also undecidable.

Only in the general case. In many/most loops that humans would find useful in practice you can prove termination.

In general case, yes, of course.

There are still cases where you can prove that a recursion is bounded (I suppose something like dependent types could help here). There are definitely cases where you can prove that a loop is bounded, because the semantics of the language requires them to: a loop with a counter (not otherwise mutated), iteration over a known finite structure, etc.

Well, both C++ and Haskell allow you to use compiler features that are undecidable in general case, but usually work well in practical cases. Also, if e.g. your recursion / loop analysis is taking too long, you can just stop the analyzer. If the code can't be reasonably proved right, it should be considered wrong (with a chance of a false negative).

You might be thinking of Total Functional Programming [0] "a programming paradigm that restricts the range of programs to those that are provably terminating."

[0] https://en.wikipedia.org/wiki/Total_functional_programming

But the comment here at the top was "how are we going to deal with these things at the language level?" and the implication that there are no understood strategies for tackling this problem.

Getting people to use heavy static analysis is an uphill battle. Getting people to use prepared statements to prevent SQL injection is an uphill battle! But nobody should take then lesson that we are woefully unprepared to deal with timing leaks via program analysis and that we've entered some new unfamiliar territory.

Time leaks are not fundamental to computing. They can be fundamental to running concurrent adversarial processes on the same core, though.

Indeed, having no speculative execution, or just having caches separated by trust domains, would make Spectre impossible. This would make the whole promise of 'securely virtualized hardware' largely disappear, though. For guaranteed isolation, you'd have to have a physical core (or set of cores) per trust domain.

With trust domains sliced pretty thinly, e.g. a domain per JS-executing web page, it's hard. AFAICT, reseting the caches when switching processes (that is, trust domains) sort of mitigates this attack at a relative low cost, a performance hit instead of having to replace the CPU.

> Time leaks are not fundamental to computing.

Ok, fine, in some abstract sense. But they are fundamental to realizations of computing that involve shared resources, as the rest of your comment is getting at.

We want to share resources for efficiency, which is going to be the constant pressure that keeps leaks coming.

Sure, there's a pressure for performance figures that makes hardware makers cut various corners, including security. Same with software.

Reality is always about compromises and tradeoffs. Now we see how the balance point is being pushed back closer to the pole of "security". A new equilibrium will eventually appear.

(You can see the very same process in e.g. encryption algorithms: tradeoffs between performance and security, and phasing out of solutions that yielded either to finding of logical flaws or increases in available computing power.)

Currently we build CPUs with a handful of very powerful cores and multiplex processes onto them, to optimize for the use case that a process really does need all the power a core offers. We could build processors with, say, only two powerful cores and a hundred simple cores and give most processes their own core.

That's either a big waste of silicon or a very hard problem.

On a related topic, I know someone who worked on CPU/FPGA hybrid architectures. The idea was to move processes between CPUs and FPGAs. Awesome stuff, realtime processes offloaded to the FPGA get to run completely off the CPU, with ridiculously low latencies. The issue is that you really have to design your code for it.

FPGAs are great because they are field-programmable and can adapt the hardware to a task. In all other aspects (density, power draw, cost) they are not that great.

We could consider something like Tilera chips working together with privileged "general compute" chips, the same way as current machines work with separate GPUs as privilege "vector compute" chips.

I still dream of a day where the compiler largely handles this kind of thing for you. I'm starting to suspect that this day may never come, but it feels like a logical extension of the jit. To have code that self modifies not just itself to run faster, but also the hardware it runs on just seems so cool.

Course, in the context of the larger thread, I can't help but wonder how much more attack surface this would tend to create.

I remember something marketed as a “hypercomputer” by Starburst Systems or something like that (long since defunct, apparently... I'm referring back to the late 1990s and early 2000s) that “compiled software to hardware” by substituting parallel CPUs with FPGAs.

This approach has been tried - as it turns out, we're not very good at writing compilers.

Compilers are sort of at the edge of technology, there is always some value in trying again, no matter how many times it has been tried before.

>> That's either a big waste of silicon or a very hard problem.

How about 16 big core and 4096 small cores that don't have speculative execution?

https://content.riscv.org/wp-content/uploads/2017/12/Tue1136...

Perhaps one day we'll talk about how many cores are allocated to a program rather than the other way around. OTOH even their chip will have shared caches. Spectre is achieved via speculation but communicates via side channel of the cache, so it's not clear this is a whole lot better.

There are always things that are shared even between distinct cores: RAM, buses, disk I/O, network I/O, LAN, the Internet, etc.

Agreed. I pointed out caches. Running only a single process per core does prevent sharing of the branch predictor and the lowest level cache.

What nobody wants to say is that the real problem is running untrusted code. They don't want to say it because Apps and JS are so many peoples bread an butter these days.

"Time leaks are not fundamental to computing. They can be fundamental to running concurrent adversarial processes on the same core, though."

Wrong.

Even if you separate different privilege levels onto different physical computers, and they only exchange information by message passing, then they are likely to leak information merely from the message timing.

The message timing may indicate what has been cached or pre-computed on the privileged machine. So it's a matter of sending messages from the malicious machine such that they manipulate what is cached/pre-computed on the privileged machine based on the contents of privileged information.

Manipulating what is cached/pre-computed is generally not too hard for an attacker; the real trick is doing so based on the contents of privileged information. But it's conceivable that you could extract some information from a database by determining which pages of a btree got cached when you try (and fail) to look at something you're not supposed to. It might be hard to extract the 1000th byte of a big text field that way, but you might be able to find out whether "joe" or "sally" is the person you're looking for.

Sounds a bit difficult in practice, but computing (perhaps more than any other field) tends to quickly eliminate the difference between theory and practice when the motivation is strong enough.

Timing attacks for e.g. password cracking are well-known. This is why most of the security-related computations go to great lengths to make computation-time strictly data-independent. Adding an arbitrary / random delay on failure is also know.

The more you trust the code you run alongside other code, the less precautions like that you have to take. Delimiting security domains right is hard, though.

A "security model" like a memory model should be able to tell you the guarantees available to shield a process from another process upon execution of an instruction. I think a memory model already does this to some extent, just not as everyone thought for speculative execution and side channel timing attacks. A quick Google search will show research on static analyzers for side channel timing attacks, as others have said, on the same core. Having clock strata are also not a new thing, it is resource intensive for make available a more accurate clock, and much cheaper to provide an inaccurate clock.

As far as sharing cache goes, there can be 4096 PCIDs/ASIDs AFAICT, maybe there should be more. Tying speculative execution to PCIDs/ASIDs might not be too bad of an idea.. if it isn't done already. Better CPU security models that reason about cache and speculative execution should be enough to solve this problem.

Deal with them on OS/VM/sandbox/"system" level. Treat time measurement as privileged. Make it really hard to get precise enough timing in untrusted processes.

Disable TSC access, lower clock_gettime precision, make clock_gettime return fuzzy (randomized) time. Randomize CPU frequency to make usage of spinning threads for time measurement hard. Insert randomized delays into untrusted binaries, kinda like DTrace inserts probes (i.e. imagine a JavaScript JIT that inserts no-ops all over the compiled code, and randomly changes these to random sleeps). etc.

But those are all just mitigations, not fixes. Such changes don't guarantee that it's impossible to still leak information - just that it will be harder (but not inherently impossible) to exploit.

If you increase the number of bits in a hash, you do not guarantee against collisions, but you can make them so infrequent that searching for them becomes impractical.

If the randomizations have such an effect that data sniffing is still possible but its speed is 1 bit per week, trying to sniff something interesting becomes impractical. (Or not; depends on your threat model.)

The root of all evil is nondeterminism. A program which executes deterministically cannot receive a timing channel! So "all" we have to do to end this entire class of problems is deny all nondeterministic features, including shared memory threading and timers and two way network communication, to all untrusted code.

A practical vision of computing without these things is challenging, though!

Yes exactly, the problem is non determinism. But I think it should be possible to have deterministic execution while still keeping compatibility with existing software, by replacing the real time with a "fake" time that is deterministic upon the stream of instructions executed, which is on average close to real time. This requires support by the CPU, but it is a relatively simple change, compared to changing speculative execution and caching. Fake time could be kept in sync with real time, by periodically running a privileged process that takes a fixed amount of fake time, but variable amount of real time. (I brought this up in a different comment thread that got marked as duplicate.)

... and then you have to make, for example, scheduling of threads based on "fake time".

rr does just this! I think it uses the "instructions retired" performance counter as its "fake time"; that turns out to be deterministic enough for its purposes. Whether it's deterministic enough in a security context, I don't know for sure.

But this approach, though it can run threaded software, will not let untrusted software (which should really mean all software!) use more than one real core or hardware thread.

What's rr?

found it: https://github.com/mozilla/rr

We can also try to avoid concurrently executing untrusted code on a single processor?

At least on the server side, that's realistic. Big companies like Google already run their own trusted code on their own hardware. For everyone else, it's not impossible to move from VPS hosting to "bare metal cloud" like Scaleway offers.

(Vision for the Future™: instead of their tied-to-Linux "someone else's Raspberry Pi" experience, it would be a bunch of tiny single core processors, each connected to their own tiny DRAM chip. You upload unikernel images or CloudABI binaries (that would be then wrapped into unikernels) into the Cloud™, where the load balancer boots up your images on-demand on as many of these tiny computers as needed. RAM is zeroed before boot.)

The other big environment with tons of untrusted code is of course the web browser. This is significantly more ridiculous, but: why not embed a ton of tiny simple in-order ARM cores without any shared cache into desktop processors, and run JS/WASM on them? (One core used per origin per site) :D

> The other big environment with tons of untrusted code is of course the web browser. This is significantly more ridiculous, but: why not embed a ton of tiny simple in-order ARM cores without any shared cache into desktop processors, and run JS/WASM on them? (One core used per origin per site) :D

I definitely chuckled. :) On a more serious note- I'd bet at least a couple bucks it would be possible (albeit super weird and difficult) to channel information through hardware-acceleration mechanisms. Lots of rendering happens on the GPU these days.

> A program which executes deterministically cannot receive a timing channel!

Only if you define 'deterministically' to mean 'determined only by the program's own legitimately accessible context'. These timing side-channel attacks work precisely because the processor performs in a deterministic and detectable manner, but does so based on information which the attacking program should not be able to access.

No, hardware bugs could work like you describe, but Spectre/Meltdown does not make the result of executing a program depend on the results of speculative execution. It just makes timings depend on such results. If you can't time things, which a deterministic program can't (access to any real timer makes a program nondeterministic), you can set up spectre attacks but you can't receive the results.

It won‘t work. The mechanism that hides the timing information from untrusted code will itself leak timing information.

You just need to refine statistics. The underlying program can‘t be solved in a physical universe.

All interactive programs are nondeterministic. If you remove all other timers, you can still tell the user to click something and see how much work you can do before they click it. That's an exceptionally noisy timer, but a timer nonetheless. The only way to completely remove timers is to revert to batch mode programs.

If you buffer all I/O until the program has finished executing, I don't think this type of timer works. (The message to the user is displayed only after the process you are trying to time completes, and then when the user clicks the button you are executing again)

The program is equivalent to a pure function from (state, events) to (state, actions) and the computing device that evaluates this function can't leak any information to the function without evaluating it incorrectly. It can still leak information in how long it takes to evaluate the function, but there is no direct way to get this information back into the function.

You could ask the user what time it is, or how long something took, but that starts to look suspicious fast!

But shared information is not restricted to shared memory in a computer and it’s threads. As soon you interact with some other system you will have this problem, in a database or any other non trivial (non computer) system?

Timing doesn't have to be in seconds. You can spin up a second thread, that increments a variable and use that a your meter stick for elapsed time. Another though is to have the timer on some external server.

This wrecks a lot of useful things and doesn't really address the problem.

Please no! Some of us need to do performance analysis. Surely the proper fix is to not expose the sensitive information, rather than to try to constrain the attacker's ability to see it easily?

Given that "silicon is cheap" why don't we work around these problems by ensuring that processes within different security domains run on separate cores with their own cache and branch prediction cache? At context-switch, flush all that.

We need to do performance analysis, but sandboxed code usually doesn't. The performance measurement can be in the environment.

This is similar to eval(). The operating system always needs a way to load new code, but you don't need it in the language, or least not in a sandboxed language.

It's also more consistent with the abstract programming model that we typically use. A new version of a function is normally considered compatible with the previous one based on the values it returns, not the details of its timing (within reason).

We often depend on this correctness vs. performance separation to be able to make performance improvements easily. It's very convenient to be able to swap in faster code without worrying that you'll break any callers. It's also convenient not to have to write constant-time functions (to avoid information leaks) most of the time.

Yeah, and for developers of sandboxed code (i.e. JS/WASM in webpages) precise timing should be available in a special Developer Mode.

Or just include the timing in your models, and derive from those models a suite of tests that can be run on the hardware to verify that the timing is as it was taken to be in the proven system?

I agree with the gist of your comment but pedantically want to take issue with this ;) :

> That is, the basic premise of hardware process isolation is that a process cannot have any knowledge of what another process is doing, or whether it even exists,

Side channels such as the cache and timing break that promise.

This has been known forever. Nobody can contemplate a decent CPU without cache!

The thing that spectre and meltdown have demonstrated - obvious in hindsight! - is that CPUs that speculate can use this side channel to exfiltrate secrets in shockingly powerful ways that are really hard to defend against.

We can do things to stop speculated loads leaking via cache hoist/mru/evict/etc and make chips immune to these powerful attacks.

Eliminating the general cache side channel is a damn sight harder and still an open problem.

The cache attacks against crypto systems eg scrypt are fascinating just like spectre.

To summarize, if I may, your observation using the familiar template:

Low-latency memory access, low-latency conditionals, secure isolation ... choose two.

>> Nobody can contemplate a decent CPU without cache!

I like to contemplate a huge SRAM on die. Get rid of caches and speculation entirely. Of course that doesn't work for really big systems, but we might one day have a full 32bit address space available like this. Now hopefully you can contemplate it too!

> Spectre has nothing to do with program correctness or safety.

Unless your program is a VM for a programming language (e.g. JavaScript) that runs code from different origins in the same protection domain. Even perfect hardware process isolation won't help you solve that problem.

Of course it will! Spawn a separate process with a JS VM per page, on a separate core if you can afford, and the problem goes away.

The price is steep, though — at least with the current crop of hardware.

I did say a single protection domain, because it seems unlikely that any popular web browser is going to switch to a model where DOM access requires IPC.

That said, even a single VM per page doesn't help, because you have scripts from advertising networks running alongside other scripts. You'd need at least a VM-per-origin-per-page.

This depends on the threat model. E.g. running the JS VM on a separate hardware host under a stripped-down supervisor would prevent any web page from stealing secrets from your "main" machine, but not from each other.

I suppose that once a page includes third-party scripts, it already gives them the key to its kingdom, like sniffing anything from DOM or altering it in arbitrary ways. Thus per-page isolation seems sufficient to me; maybe even per-page-set isolation when I open many pages from the same site (this needs a way of clearly defining what "the same site" is).

> I suppose that once a page includes third-party scripts, it already gives them the key to its kingdom, like sniffing anything from DOM or altering it in arbitrary ways

doesn't same origin policy prevent this?

No, loading a script (from anywhere) effectively invites it into the origin of your page, giving it access to everything connected to the origin of the page. That is, the origin of the script is not considered, only that of the page.

Think about loading jQuery from a CDN, for example, which people do. If third-party scripts couldn't access the DOM it wouldn't be very useful.

What about web workers or service workers? Don't browsers force all script execution in the workers into a separate process?

>Spectre has nothing to do with program correctness or safety.

I get your point and also your analogy of the "bricks::hardware" and "house::software".

Yes, Spectre has nothing to do with C/C++/Javascript/Rust safety. Yes, we can look at the world as it currently is with existing languages and confidently say that.

However, I think you're inadvertently creating a thought-stopping comment instead of charitably reading his essay as exploring a possible future of language security and whether that langsec evolution is practical or provable. That author starts that line of thought with, "Where do we go from here? I see but two options. [...]"

My attempts at addressing the author's possible future would be:

1) microcode instructions may be considered a "competitive advantage" and therefore cpu manufacturers like Intel and AMD wouldn't publicize them such that GCC/Clang could incorporate that intelligence into a compilation algorithm. There are already variations of this profit-vs-openness tension happening such as NVIDIA not releasing open source Linux drivers.

2) publishing microcode architecture and putting the optimization responsibility into into GCC/LLVM sounds very similar to the failed EPIC instruction set[1] for Itanium. There seems to be an underlying human law of "specialization" and having Intel hardware engineers figure out all the speculative out-of-order-execution was better for us than having Richard Stallman and his gcc colleagues work on it. Unfortunately, the hardware side of things created a 20 year old bug. Is there new evidence about the interaction of hardware optimization & compiler theory that won't repeat the Itanium EPIC failure?

3) having a completely specified "hardware model vm" transparent to a compiler and language spec doesn't necessarily remove side-channel attacks. It may just change who creates the vulnerabilities... e.g. the Clang LLVM team (instead of Intel) inadvertently creates a timing attack inside the target executable.

[1] https://en.wikipedia.org/wiki/Explicitly_parallel_instructio...

Isn't "not publishing microcode instructions" security by obscurity?

> Yes, Spectre has nothing to do with C/C++/Javascript/Rust safety.

I'm not so sure at the root cause level, part of the problem is that programming languages treat memory as a contiguous blob and speculative execution is a work around for that. All languages are designed as if the memory bus speed and cpu are still identical. Maybe languages need better ways to tell CPU's what data they are going to need ahead of time so that the CPU can have it ready.

Could we build a cache aware programming language? Imagine something like an iterator that would process one item and concurrently pull in data for the next iteration. If creating correct hardware is too hard then maybe we can be more explicit at the software level.

"Preloading" instructions already exist, e.g.:

http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc....

I was thinking something slightly more complicated. Correct me if I'm wrong but you have to know the memory address to prefetch so it can only deal with a single level of indirection. Often it's a case where you know you'll need x but you'll also need x.y (and y is a pointer) and you can't prefetch that until you have x. For many cases you could build an index to get both efficiently but I think it's pretty hard to do generically.

> Spectre has nothing to do with program correctness or safety. It has everything to do with hardware's correctness and safety.

Yes, but safety is safety. The point of the article is that the assumption on the part of language nerds for the past few decades -- that correct choice of processes and implementation patterns as expressed by whatever favorite runtime the author wants can protect us from security bugs -- turns out to be FALSE.

Rust and Haskell programs are subject to Spectre attacks just as badly as K&R C ones from 1983. All that pontification didn't actually work!

The point is that it puts a limit on pedantry about "correctness". That's all based on an idea about a "computer" being an abstracted device, when it turns out the real-world machines are in fact leaky abstractions. The lesson to my ears isn't that you shouldn't use Rust or whatever, but that some humility about the boundaries of "correctness" would probably be a good idea for many of the pontificators.

> All that pontification didn't actually work!

This is a bit silly. Security is a chain that is only as strong as its weakest link. For decades we believed that C was the weakest link, and now, with Spectre, we have discovered (drumroll, please!): nah, C is still the weakest link. For all the amazingly scary things that Spectre brings to the table, it's still less scary than Heartbleed and Cloudbleed were.

Don't get me wrong, hardware still sucks (and with Intel and AMD's growing body of management engine incompetence they may yet overtake C as the weakest link in the chain) but we will learn from this and get better. In the meantime, we need to be pushing forward on all fronts: hardware security, language security, kernel security, application security, network security... nobody gets to stand still.

Long before Heartbleed or Cloudbleed researchers (and presumably attackers) were using remote timing attacks to extract secret keys:

  https://crypto.stanford.edu/~dabo/papers/ssl-timing.pdf

And most big data breaches where information assets are actually stolen involve services written using "safe" languages, like Java or SQL.

And even if C is the weakest link, all that means is that you're totally screwed. No amount of Rust will save you when the Linux kernel, your relational database, and every router between you and the attacker are written using C or assembly.

At the end of the day, if you want strong security assurances you need to prove the correctness of all the semantics (of which memory bounds constraining is but one small aspect) of every piece of software in your stack, or at the very least all the most critical pieces. And the best tooling for that is for Ada and C.

> some humility about the boundaries of "correctness" would probably be a good idea for many of the pontificators

I'm probably biased, but in my experience the people actually pushing for correct-by-construction tools tend to be acutely aware of the limitations of their approach, especially when it comes to having to trust hardware to do what it says. For example, all of the people I've seen advocating for seL4 tend to be very transparent that their proofs assume hardware correctness and that they don't think it's realistic to exclude much of the hardware from the trusted computing base. Further, it seems to me that the Rust developers have been extremely pragmatic about what is possible to mitigate and what they have to trust the hardware for.

I'm sure there are some examples of what you're describing, but without any sort of references, the generalizations you're making have a whiff of bad faith.

> Rust and Haskell programs are subject to Spectre attacks just as badly as K&R C ones from 1983. All that pontification didn't actually work!

Um, Rust and Haskell aren't about security against malicious attackers exploiting hardware/system flaws. They are about correctness against programmers writing (some classes of) bugs by mistake. The two aren't directly related. Program correctness is a worthy goal even if it doesn't protect you against hardware problems.

Except that they go annoying everyone with their memory safety as if it was a huge breakthrough, when in fact most of the serious information leakages do not originate from such problems but simply from design errors.

Same goes for the proponents of formal stuff like Coq. Even worse, because those languages are so insufferable that they induce design errors, the number of which will grow each time a poor soul will have to maintain the... thing. Then, all right, there is no mistake, the result maps perfectly to all your design errors.

Design errors are a class of mistakes. Nobody can help you with design errors. Functional programming, immutability, static typing et al address other kinds of mistakes.

> when in fact most of the serious information leakages do not originate from such problems

We've already established that the parent post made a mistake in thinking FP is about safety against attackers / information leakage. Why are you still talking about this?

> because those languages are so insufferable that they induce design errors

[citation needed]

What's your actual experience with these languages?

I came by to say essentially the same thing. The article is complaining that CPU behavior is treated as axiomatic by software but that treatment is flawed because the CPU may not satisfy all the conditions of its assumed behavior.

I have had the experience of seeing the 'sausage making' of CPUs on the other side when I worked at Intel and the verification of the 80286 was a big thing and the evolution of the 80386 was just starting. And the sad truth is that hardware engineers, exactly like software engineers, are often compelled to accept a 'good enough' solution when the business decides they have reached that point of what the business is willing to invest against the expected monetary returns.

In software this will express itself as an algorithm that is correct 99.99% of the time. Or one which is computationally expensive and so replaced with an algorithm that takes less computation but gives good enough results. And in the normal course of things, those decisions are often "ok" because failures are rare and when they fail there isn't any "gain" by them failing.

Security of course turns that calculus on its head, where, if you can break the chain somewhere, you win. So a place where the chain is only 99.9% as strong as it is elsewhere will get special attention. And when the chain breaks there is gain that exceeds the effort involved.

For much of the behavior that is responsible for both Spectre and Meltdown, the CPU can be constructed to not bypass the other secure checks. If the designer chose to, they could have the CPU machine check or fault if it read protected memory in a speculative path. Even if that path wasn't actually taken.

I don't know of course, but I would expect the typical conversation at a CPU design house would be, this;

A) We should always fault if we access protected memory

B) But what if its just an uninitialized pointer on a branch that won't be taken?

A) It is still a fault.

B) Ok but really "only" if we take the branch so lets wait until the code is actually executed to fault. Tree in the woods with no one around to hear it and all that ...

Good engineers, designing cool machines, making completely reasonable decisions about what is 'good enough', against a spec that says "CPU will fault if it ever accesses protected memory." because it will fault if the code ever gets there. As opposed to designing the fetcher to always check memory protections and always fault. To any reasonable person, both would seem to be sufficient, but only one is correct. And since it takes more silicon and more complexity to always check, we get the one that is good enough. It is my hope that at this very moment there are CPU designers all around the world changing the HDL in their design to be correct, and verifying that they run just as fast as they did before, just that now your CPU can fault on an address that wasn't actually executed. I am looking for any example where speculative execution or fetching of protected memory is ever not a 'bug' waiting to happen in a piece of code.

As a result I expect CPU designs to be updated, and new micro-architecture where this behavior always faults but is otherwise just as performant. No doubt it will take some additional transistors.

A mispredicted branch is incredibly likely to perform operations that would normally fault (consider misprediction of a null pointer check, for example...) I don't think it's feasible to have a (useful) version of speculative execution that can trigger a true fault, because the mispredicted branches are going to violate all sorts of software invariants.

NULL is an interesting case. I'm not sure how Linux handles it but in some OSes there is a page table entry for virtual address 0 for just this reason. You have to assume that bugs will access it. I'm wondering about pages that are outside of your allocated address space.

> I am looking for any example where speculative execution or fetching of protected memory is ever not a 'bug' waiting to happen in a piece of code.

Um. Allocate a page of memory and then write to it (e.g. memset(mmap(NULL, PAGE_SIZE, PROT_WRITE, MAP_SHARED | MAP_ANONYMOUS, -1, 0), -1, PAGE_SIZE). Each time the CPU hits the loop condition in memset it will speculate the loop to continue and write to the next byte of memory (or more if unrolled). When it hits the end of the page the speculative execution will attempt to write to an unmapped page (or worse), but that's fine because the loop condition is falsw and so the write isn't retired.

If you can't speculate that a loop that has run 4096 times will continue another iteration, what can you speculate?

Your correct I wasn't specific enough in my question. I should have included the qualifier 'in unprivileged code' after 'protected memory' up there.

I really like that example because it's completely reasonable for real world software to do, and the speculative execution would run off the page every time. Loops copying data end in speculative reads, and we like to align structures to power-of-two sizes for cache friendliness.

A way of reformulating the author's argument is to recognise that there exists an intermediate block of programs that do not appear in any source-code, and that's the re-scheduler in the CPU, and that you can't reason deterministically about its behaviour, because its state is common to all the processes hosted on the system at that moment in time.

Formulated thusly, the author's argument seems eminently valid to me, and exposes the old bug-bear: the root of all this evil is nondeterministic execution. Elsewhere in this thread I bemoan the defunct IA-64 (Itanium) architecture because it delegated explicating inherent parallelism to the compiler and allowed the core to be shorn of rescheduling circuits, and (it now emerges) enhances security.

> Spectre has nothing to do with program correctness or safety. It has everything to do with hardware's correctness and safety.

But that “hardware” is mostly a program running on a machine whose ISA you don’t know. Intel is shipping a microcode patch.

In an earlier life I wrote microcode, as well as programming machines whose ISA could be changed by rewiring the backplane (PDP-10). I used to think I “knew the machine” and, in today’s parlance, “the stack” as well. Not anymore — nobody can grasp the entire stack.

The opening line that "The work of engineers used to be about taking small parts that they understood entirely and using simple techniques to compose them into larger things that do what they want" is not correct. Emergent behaviour has always been an issue for complex system. Just look at the story behind the Tacoma Narrows Bridge.

Computing is extremely complex, so the issue is probably more acute, but it is not unique.

I agree with you. Engineers of physical things don't fully understand what steel is made of (since we don't fully understand the lowest underpinnings of matter or all of its properties).

OK so do we finally get proper lisp machines now?

Lisp machines (at least, Symbolics Lisp Machines which I know well) didn't suffer from these flaws. They were largely designed to be single-user machines and there was literally almost no isolation between anything!

But weren't Symbolics Lisp Machines from an era where nothing suffered from these flaws, because nothing did speculative execution?

As far as I know, this is true for the Symbolics Ivory CPUs, yes. That said, these flaws would be irrelevant, if so, because the system built upon the hardware did not enforce modern process isolation paradigms.

> there was literally almost no isolation between anything

The CPU knows the type and size of everything. It also checks that at runtime. Every piece of data has type and size information (either implicit or explicit).

On a conventional CPU you can access memory of an array (usually CPUs don't even have an idea what an array is) without checking its bounds - unless the language implementation explicitly creates those bounds checks and provides the array size at runtime.

On a Symbolics Lisp Machine the array will be passed with type and size info and the CPU will check that when accessing the array.

Security by proof, model checking, semantics is still a good, effective tool!

Leveraging the type system is a good communication channel for programmers maintaining the system.

Proofs and models of the protocols are still important.

But yes... we still need to fix CPUs. And the class of errors (those of omission) are still worth removing from our code regardless of spectre or meltdown.

Security is an emergent property of a system consisting of users, software and hardware. Thus, a programmer cannot prove security of a system but merely assert its certain behaviour. Langsec does just that. No, it can never be used to build secure systems. Yes, it can be used to solve practical problems making things more secure.

The author of this post isn't properly characterizing langsec:

The basis of language security is starting from a programming language with a well-defined, easy-to-understand semantics. ... This approach is taken, for example, by Google's Caja compiler to isolate components from each other, even when they run in the context of the same web page.

From what I can tell, he's talking about the broader area of "programming languages and security". That is not the same thing as http://langsec.org/, which is essentially about using grammars to recognize network PROTOCOL formats.

As far as I remember, one motivating vulnerability is that there were two different parsers for SSL certificates, which allowed attackers to trick browsers into accepting invalid certificates. That doesn't have anything to do with programming languages per se; you can write this vulnerability in any language. It's analogous to the fact that using a safe language doesn't prevent you from SQL injection.

Some examples of what they are trying to address:

http://langsec.org/papers/langsec-cwes-secdev2016.pdf

I wrote a critique of langsec a few months ago here:

https://lobste.rs/s/uyjzjc/science_insecurity_meredith_l_pat...

tl;dr I think they are using the wrong formalisms.

I found it odd that the author was assuming that langsec is a widely used thing when I think it is nascent research.

Even Google Caja, a totally different project outside of langsec, is not widely deployed, although I very much like its ideas.

Just FTR, your critique is answered by Stefan Lucks, Norina Grosch, and Joshua Koenig's paper[0] from last year's langsec workshop at IEEE Security and Privacy. They define a formalism, calc-regular languages, to handle length-prefixed strings.

[0] http://spw17.langsec.org/papers.html#calc-regular

Thanks, this looks promising! I'll take a look.

Hi Andy, thanks for writing this.

I don't think we are fundamentally hopeless for "langsec", although history will definitely be divided into two Epochs: a time before Spectre and a time after.

Language runtimes and operating systems just got some really great new research problems, and a lots of interesting ideas are afoot (many in V8 land).

There is no way that this is true. The program analysis community has known for decades that systems were only ever sound w.r.t. some assumptions. See Andrew Appel's paper on breaking java safety with mcdonalds heat lamps from like a decade ago for a fun example.

Basically every static analysis person I've talked to about this agrees that it is a really really cool attack but that it doesn't represent fundamental new information for the field.

I think there is a deeper truth here - understanding of what the hardware is doing has always been essential for writing correct, secure, performant programs - and it is the (IMHO, mistaken) ideology that this is not the case that took the biggest hit from Spectre/Meltdown/et al.

> One manifestation of the Spectre vulnerability is that code running in a process can now read the entirety of its address space, bypassing invariants of the language in which it is written, even if it is written in a "safe" language. This is currently being used by JavaScript programs to exfiltrate passwords from a browser's password manager, or bitcoin wallets.

Isn't this incorrect? I thought it was Meltdown, not Spectre, that was being used to read the browser's password manager from JavaScript, and that Spectre-via-Javascript was limited to reading data within the same JS VM process (so e.g. you could prevent Spectre from reading cookies by making them http-only). This matters because meltdown is much easier to patch than Spectre.

This is like saying a compiler bug in a safe language ends langsec. Which is obviously absurd. It means the implementation had a flaw, but that doesn't make the whole thing worthless. And when the flaw is fixed the same guarantees are restored.

The problem is that what you call guarantees weren't guarantees to begin with, and we can't be sure they are now.

That's true about any engineering artifact though. If your steel rebar isn't built to whatever standard you require your concrete skyscraper isn't going to be structurally sound. To build on top of the layers below you, you have to trust that they work, and when problems occur you fix the problems as they come up (or ideally prevent them ahead of time).

I am not seeing the connection to LANGSEC. The Spectre and Meltdown attacks turn the processor into a confused deputy, that is all. If anything, this is predicted by LANGSEC. The beef is not even with hardware verification, as some have suggested, because the specification never calls for such security guarantees. The specification is architectural because we want different processors to implement the same architecture, such that they are compatible. The only reason transient instruction sequences have security violating side effects is microarchitectural leaks.

I think concluding the "end of langsec" goes too far. We'll continue to need both langsec, plus much more thorough hardware verification to re-establish basic isolation assumptions lost with Spectre/Meltdown (or push for detailed HW specs to begin with, to be able to assert these assumptions on our own).

OTOH, as if it wasn't obvious enough already, I'm seeing a serious issue with the concept of executing arbitrary code from untrusted network locations, such as with JavaScript on the Web.

The failure lies in forgetting that computers are not deterministic machines, they are probabilistically deterministic machines instead.

They are physical constructs, not mathematical ones, and as such, verification is inescapable if you want some level of assurance. You need tolerances and experimentation after construction, even if you proved your thing correct.

In the words of Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."

The major chip manufacturers need to have two kinds of cores/caches. One that has full security guarantees, the other that is optimized for energy efficiency/performance and has zero interprocess security. This isn't a one size fits all problem.

I see some people assume that a possibility of a single chip that can do both is not option. It is. It's only x86 that has to do everything in hardware and hide everything from the user for backwards compatibility.

Imagine instructing a compiler for an architecture that does everything in software, like Mill, to make every operation constant time or to speculate aggressively and unsafely depending on what the program needs.

Even on the Arduino I don't think I could claim that I knew 100% what was going on, let alone go/python/JS -> kernel -> docker/VM -> -> kernel -> processor

meh.

reasoning always loses out to empirical techniques anyway.

Buy a new cpu that is fixed and problem gone maybe we shouldn’t change the world maybe intel should fix there own problem? If a car has a serious fault that makes it dangerous it’s recalled it’s time for intel to do the same.

Reply on news.ycombinator.com