Use verifier to identify dependent reads that require speculative load hardening

[Alan-Jowett]

Use verifier to identify dependent reads that require speculative load hardening

The verifier has the context required to identify dependent loads that require speculative load hardening. Rather than rebuild this context in the jitter/interpreter, the verifier could provide the interpreter/jitter the list of instructions that require speculative load hardening. It's possible that the existing CFG has enough information, but it's not 100% clear.

See this link for details about the problem: https://googleprojectzero.blogspot.com/2018/01/reading-privileged-memory-with-side.html

See this link for details about the speculative load hardening: https://releases.llvm.org/8.0.1/docs/SpeculativeLoadHardening.html

[dthaler]

The project already exposes prepare_cfg() separately from ebpf_verify_program(). (The check utility calls the former for the "cfg" domain and the latter for the "zoneCrab" domain.) So I think this is just a question about whether the existing cfg_t returned from prepare_cfg() already has sufficient information, in which case no change is needed, or not in which case this is a feature request to add more info into the cfg_t info.

[Alan-Jowett]

I think the CFG isn't enough as we need to know when an branch is conditional based on an untrusted value and when a load is from memory shared with user (i.e. map value memory). If that info is present in the CFG I am not understanding it.

Conditions appear to be: 1) Use of an attacker controlled / untrusted index. 2) Dereference of memory using the untrusted index. 3) Use of the value from 2 to dereference memory shared with user mode.

Seems like we need the following: 1) Mark blocks that are conditional based on untrusted data as untrusted blocks. 2) Any values loaded from memory inside an untrusted block are untrusted values. 3) Loads from map value using untrusted values must be lfenced.

Simplest solution: Loads from map values get tagged for lfence.

Downside would be that this would penalize safe loads.

More performant: Loads from map values in untrusted block get tagged for lfence.

Downside would be it's still overly broad.

Most performant: Loads from map values whose index is untrusted get tagged for lfence.

Downside would be that this is the most complicated.

[caballa]

@Alan-Jowett : it seems that you want some kind of taint analysis, right?

[elazarg]

Some thoughts:

• It is an optimization step, essentially creating an intermediate representation of eBPF - one augmented with optimization hints to the AOT compiler. Not necessarily a bad idea in general, and there could be a lot more optimization hints, such as the results of the strict flag from #175. If I'm not mistaken it would require some form of certificate.
• This concept is somewhat architecture dependent, I think, but maybe PREVAIL can do the architecture-independent part of it.
• It seem to require taint analysis (in addition to tracking what memory region is accessed) which is not something PREVAIL currently does.

I think such taint analysis may be performed by adding a fourth kind of variable, a boolean user_controlled, in addition to the value, the offset and the type. This has performance implications on the verifier itself, though it might be possible to do it in another pass, like some sort of constant propagation, so it could be fast.

I don't think we should do this soon, though.

[elazarg]

The specte branch is an initial work on this.