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.)

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.

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

"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)

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.

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.

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.

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.

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.

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.

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

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

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.

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.

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.

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?)

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.

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.

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.

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/.

– Gregor Kiczales, 1992

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.

> 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.

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?

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.

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.

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.

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.

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"?

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.

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.

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 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.

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)

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

Will this be sent to the mailing list when released?

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.

    if (index < bounds) {
        index2 = array1[index];
        ... array2[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.

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 ;)

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/

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.

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

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.

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.

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.

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.

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.

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.

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.

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 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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.)

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.

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.

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

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

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.

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.

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.

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!

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

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.)

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.

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.

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.

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.

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.

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

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.

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

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.

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.)

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).

> 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.

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

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!

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...

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.

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

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.

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.

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.

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

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.

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).

doesn't same origin policy prevent this?

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.

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.

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?

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.

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.

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

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.

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.

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.

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.

> 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?

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

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.

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.

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.

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

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).

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.

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.

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.

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."

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.

reasoning always loses out to empirical techniques anyway.