Thanks Kent and Gerwin! To Kent's question about how I found the issue with x86_read_fs_base_impl: it wasn't the result of any static analysis, just something that I stumbled on while browsing to figure out how segment registers are handled ... and Kent's description answered that nicely. Thanks specifically for pointing out RESET_SELECTORS; I missed that previously because it uses an unadorned "es" whereas I had searched for "%es" to reduce false positives; lesson learned ... On the verification side, I've long been interested in the question of how we protect against covert channels resulting from hardware state components that are undocumented, or that don't work as intended, or that are not captured in a formal model. [There was a news item in the last few weeks about a (seemingly harmless) flaw of this kind in the Apple M1 processor, which is probably why this was on my mind again.] Best wishes, and thanks again, Mark

Hi Mark,

On 24 Jun 2021, at 04:23, Mark Jones wrote:

On the verification side, I've long been interested in the question of how we protect against covert channels resulting from hardware state components that are undocumented, or that don't work as intended, or that are not captured in a formal model. [There was a news item in the last few weeks about a (seemingly harmless) flaw of this kind in the Apple M1 processor, which is probably why this was on my mind again.]

That is indeed an interesting question and it is hard to achieve. One way is doing vulnerability research to figure out where things go wrong on the hardware side and what that space even really looks like. Yuval has found many interesting side channels that way, e.g. Spectre and Meltdown are among those. Essentially this is validating the model and investigating where it breaks. The pure formal verification answer is then always a more detailed model that does have that hidden state. This works for some things (e.g. we found a missing register in one of our models that way back in the day), but it's not really feasible if there is no documentation from the hardware side or the hardware misbehaves. The other way is figuring out what we can do without full knowledge of the hardware. We have started work on that and have a few ideas that we're formalising. The end result of that if everything works out should be closing large classes of timing side channels *without* knowing the exact hardware details. The idea is that we need enough documentation to determine if an instruction *might* change some unspecified deeper hardware state (which might affect timing), and we need enough instructions/mechanisms to either partition that hardware state (as with cache colouring) or reset that hardware state (as with cache flushing). If you have both, and have a precise enough measure of time, you can build OS mechanisms that close the channels that result from that hardware state. (More in that link that Gernot sent) This would solve a good chunk of the problem -- there are more channels, such as power etc, but one thing at a time ;-) What that will still not solve is completely undocumented registers and hardware state, which I'm not sure you can do much about if you're working purely in software. It's not like these don't exist, there is a reason complex chips like modern x86 implementations have a hard time for security evaluations. You can systematically search for them as with for instance https://github.com/xoreaxeaxeax/sandsifter, but you can't know that it is complete. It's a fact of live that you must guard against some hardware-brokenness, but you do need some grounding in reality to achieve anything. Cheers, Gerwin

"Stateless shared resources are trickier (at least these cannot be exploited as side channels, but they can be exploited for intentional leakage by a trojan)." Of course. I played with that long ago... If you can observe and measure the system that contains the information and you can interact with it then you can leak information. Here we have two different attack scenarios: "remote" and "local" attacks, which are not always isolated one each other clear as some times you may found a way to start an attack vector where you are remote but the measurement is local, in example changes in the environment (radiation). "What’s really required is a HW-SW contract that guarantees that any hardware features can be spatially or temporally partitioned ( https://ts.data61.csiro.au/publications/csiro_full_text/Ge_YH_18.pdf). Then it becomes a question of verifying the HW implementation against that."" Yes, that is a very first step. And this "contract" means more and more makes sense to design both at the same time and not following complete different paths as we have been doing till nowadays. "The other way is figuring out what we can do without full knowledge of the hardware." That's a very interesting question :-). In fact, IMHO, it is also a good starting point for designing robust solutions: if your starting point is a hostile environment (unknown full hardware specs) then chances of having a more resilient solution are big. I always use that for designing my solutions: I build different layers, and assume compromise of all of them but the last one (where the protected resource is) then try to calculate what are the chances of a chained exploitation in real World. Not having full knowledge of the hardware is more than a challenge and even if I don't like to use the expression "impossible mission" I really can't figure out how to protect against hostile hardware. Just think that hostile hardware equals to have the information system roots (the physical layer) against you. I really can't figure out how anyone can protect from this, in example, from a trojaned hardware that has hidden built in mechanisms to measure environment variables. Fascinating topic. El jue, 24 jun 2021 a las 1:57, Heiser, Gernot (Data61, Eveleigh) (< Gernot.Heiser@data61.csiro.au>) escribió:

What’s really required is a HW-SW contract that guarantees that any hardware features can be spatially or temporally partitioned ( https://ts.data61.csiro.au/publications/csiro_full_text/Ge_YH_18.pdf). Then it becomes a question of verifying the HW implementation against that.

For stateful resources I actually don’t think that this would be all that hard: you’d have to show on an RTL-level description of the circuit that every register is either part of architected state or reset by the operation that removes all non-architected state.

Stateless shared resources are trickier (at least these cannot be exploited as side channels, but they can be exploited for intentional leakage by a trojan).

Gernot

...

On 24 Jun 2021, at 09:02, Gerwin Klein wrote:

Hi Mark,

...

On 24 Jun 2021, at 04:23, Mark Jones wrote:

On the verification side, I've long been interested in the question of how we protect against covert channels resulting from hardware state components that are undocumented, or that don't work as intended, or that are not captured in a formal model. [There was a news item in the last few weeks about a (seemingly harmless) flaw of this kind in the Apple M1 processor, which is probably why this was on my mind again.]

That is indeed an interesting question and it is hard to achieve.

One way is doing vulnerability research to figure out where things go wrong on the hardware side and what that space even really looks like. Yuval has found many interesting side channels that way, e.g. Spectre and Meltdown are among those. Essentially this is validating the model and investigating where it breaks.

The pure formal verification answer is then always a more detailed model that does have that hidden state. This works for some things (e.g. we found a missing register in one of our models that way back in the day), but it's not really feasible if there is no documentation from the hardware side or the hardware misbehaves.

The other way is figuring out what we can do without full knowledge of the hardware. We have started work on that and have a few ideas that we're formalising. The end result of that if everything works out should be closing large classes of timing side channels *without* knowing the exact hardware details. The idea is that we need enough documentation to determine if an instruction *might* change some unspecified deeper hardware state (which might affect timing), and we need enough instructions/mechanisms to either partition that hardware state (as with cache colouring) or reset that hardware state (as with cache flushing). If you have both, and have a precise enough measure of time, you can build OS mechanisms that close the channels that result from that hardware state. (More in that link that Gernot sent)

This would solve a good chunk of the problem -- there are more channels, such as power etc, but one thing at a time ;-)

What that will still not solve is completely undocumented registers and hardware state, which I'm not sure you can do much about if you're working purely in software. It's not like these don't exist, there is a reason complex chips like modern x86 implementations have a hard time for security evaluations. You can systematically search for them as with for instance https://github.com/xoreaxeaxeax/sandsifter, but you can't know that it is complete.

It's a fact of live that you must guard against some hardware-brokenness, but you do need some grounding in reality to achieve anything.

Cheers, Gerwin

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems