VeriFence v2 rc1 #8564
Open
VeriFence v2 rc1 #8564
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This changes the semantics of BPF_NOSPEC to always insert a speculation barrier. If this is not needed on some architecture, bypass_spec_v4() should instead return true. Consequently, sanitize_stack_spill is renamed to nospec_result. This later allows us to rely on BPF_NOSPEC from Spectre v4 mitigation to reduce complexity of Spectre v1 verification. Signed-off-by: Luis Gerhorst <luis.gerhorst@fau.de> Acked-by: Henriette Herzog <henriette.herzog@rub.de> Cc: Maximilian Ott <ott@cs.fau.de> Cc: Milan Stephan <milan.stephan@fau.de>
This is required to catch the errors later and fall back to a nospec if on a speculative path. Move code into do_check_insn(), replace "continue" with "return CHECK_NEXT_INSN", "break" with "return ALL_PATHS_CHECKED", "do_print_state = " with "*do_print_state = ", and "goto process_bpf_exit" / fallthrough with "return process_bpf_exit()". Signed-off-by: Luis Gerhorst <luis.gerhorst@fau.de> Acked-by: Henriette Herzog <henriette.herzog@rub.de> Cc: Maximilian Ott <ott@cs.fau.de> Cc: Milan Stephan <milan.stephan@fau.de>
Mark these cases as non-recoverable to later prevent them from being cought when they occur during speculative path verification. Signed-off-by: Luis Gerhorst <luis.gerhorst@fau.de> Acked-by: Henriette Herzog <henriette.herzog@rub.de> Cc: Maximilian Ott <ott@cs.fau.de> Cc: Milan Stephan <milan.stephan@fau.de>
This prevents us from trying to recover from these on speculative paths in the future. Signed-off-by: Luis Gerhorst <luis.gerhorst@fau.de> Acked-by: Henriette Herzog <henriette.herzog@rub.de> Cc: Maximilian Ott <ott@cs.fau.de> Cc: Milan Stephan <milan.stephan@fau.de>
This implements the core of the series and causes the verifier to fall back to mitigating Spectre v1 using speculation barriers. The approach was presented at LPC'24: https://lpc.events/event/18/contributions/1954/ ("Mitigating Spectre-PHT using Speculation Barriers in Linux eBPF") and RAID'24: https://arxiv.org/pdf/2405.00078 ("VeriFence: Lightweight and Precise Spectre Defenses for Untrusted Linux Kernel Extensions") In the tests, some are now successful where we previously had a false-positive (i.e., rejection). Change them to reflect where the nospec should be inserted (as comment) and modify the error message if the nospec is able to mitigate a problem that previously shadowed another problem. Briefly went through all the occurrences of EPERM, EINVAL, and EACCESS in the verifier in order to validate that catching them like this makes sense. Signed-off-by: Luis Gerhorst <luis.gerhorst@fau.de> Acked-by: Henriette Herzog <henriette.herzog@rub.de> Cc: Maximilian Ott <ott@cs.fau.de> Cc: Milan Stephan <milan.stephan@fau.de>
Insert a nospec before the access to prevent it from ever using an index that is subject to speculative scalar-confusion. Signed-off-by: Luis Gerhorst <luis.gerhorst@fau.de> Acked-by: Henriette Herzog <henriette.herzog@rub.de> Cc: Maximilian Ott <ott@cs.fau.de> Cc: Milan Stephan <milan.stephan@fau.de>
Main reason is, that it will later allow us to fall back to a nospec for certain errors in push_stack(). This changes the sanitization-case to returning -ENOMEM. However, this is more fitting as -EFAULT would indicate a verifier-internal bug. Signed-off-by: Luis Gerhorst <luis.gerhorst@fau.de> Acked-by: Henriette Herzog <henriette.herzog@rub.de> Cc: Maximilian Ott <ott@cs.fau.de> Cc: Milan Stephan <milan.stephan@fau.de>
For the now raised REASON_STACK, this allows us to later fall back to nospec for certain errors from push_stack() if we are on a speculative path. Fall back to nospec_result directly for the remaining sanitization errs even if we are not on a speculative path. We must prevent a following mem-access from using the result of the alu op speculatively. Therefore, insert a nospec after the alu insn. The latter requires us to modify the nospec_result patching code to work not only for write-type insns. Signed-off-by: Luis Gerhorst <luis.gerhorst@fau.de> Acked-by: Henriette Herzog <henriette.herzog@rub.de> Cc: Maximilian Ott <ott@cs.fau.de> Cc: Milan Stephan <milan.stephan@fau.de>
This trades verification complexity for runtime overheads due to the nospec inserted because of the EINVAL. With increased limits this allows applying mitigations to large BPF progs such as the Parca Continuous Profiler's prog. However, this requires a jump-seq limit of 256k. In any case, the same principle should apply to smaller programs therefore include it even if the limit stays at 8k for now. Most programs in "VeriFence: Lightweight and Precise Spectre Defenses for Untrusted Linux Kernel Extensions" (https://arxiv.org/pdf/2405.00078) only require a limit of 32k. Signed-off-by: Luis Gerhorst <luis.gerhorst@fau.de> Acked-by: Henriette Herzog <henriette.herzog@rub.de> Cc: Maximilian Ott <ott@cs.fau.de> Cc: Milan Stephan <milan.stephan@fau.de>
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
6 times, most recently
from
df10b88 to
16566af
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.