microsoft / sca-fuzzer

Revizor - a fuzzer to search for microarchitectural leaks in CPUs

Revizor

Revizor is a security-oriented fuzzer for detecting information leaks in CPUs, such as Spectre and Meltdown. It tests CPUs against Leakage Contracts and searches for unexpected leaks.

For more details, see our Paper (open access here), and the follow-up papers (1, 2).

Getting Started and Documentation

You can find a quick start guide at Quick Start.

For information on how to use Revizor, see User Documentation.

For information on how to contribute to Revizor, see CONTRIBUTING.md.

Need Help with Revizor?

If you find a bug in Revizor, don't hesitate to open an issue.

If something is confusing or you need help in using Revizor, we have a discussion page.

Citing Revizor

To cite this project, you can use the following references:

1. Original paper that introduced the concept of Model-based Relation Testing as well as the Revizor tool:

   Oleksii Oleksenko, Christof Fetzer, Boris Köpf, Mark Silberstein. "Revizor: Testing Black-box CPUs against Speculation Contracts" in Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2022.

2. Theoretical foundations of leakage contract:

   Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. "Hardware-software contracts for secure speculation" in Proceedings of the 2021 IEEE Symposium on Security and Privacy (SP), 2021.

3. Accessible summary of the two papers above, in a journal format:

   Oleksii Oleksenko, Christof Fetzer, Boris Köpf, Mark Silberstein. "Revizor: Testing Black-box CPUs against Speculation Contracts". In IEEE Micro, 2023.

4. Paper that introduced speculation filtering, observation filtering, and contract-based input generation:

   Oleksii Oleksenko, Marco Guarnieri, Boris Köpf, and Mark Silberstein. "Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing" in Proceedings of the 2023 IEEE Symposium on Security and Privacy (SP), 2022.

5. Paper that introduced exception-based testing (i.e., focus on Meltdown, Foreshadow) into Revizor:

   Jana Hofmann, Emanuele Vannacci, Cédric Fournet, Boris Köpf, and Oleksii Oleksenko. "Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions." in Proceedings of 32nd USENIX Security Symposium (USENIX Security), 2023.

Trademarks

This project may contain trademarks or logos for projects, products, or services. Authorized use of Microsoft trademarks or logos is subject to and must follow Microsoft's Trademark & Brand Guidelines. Use of Microsoft trademarks or logos in modified versions of this project must not cause confusion or imply Microsoft sponsorship. Any use of third-party trademarks or logos are subject to those third-party's policies.

sca-fuzzer's Issues

Arm Generator creates too many unconditional branches

Currently the Arm testcase generator seems to produce a high number of unconditional branches. This causes very little variance in the flow of generated binaries. There should be a control or change to maximize/increase the number of conditional branches.

Linux v6 compatibility issues

When I try to install executor kernel module, inpite of installing cpuid, I keep running into
sca-fuzzer/src/x86/executor/main.c:15:10: fatal error: cpuid.h: No such file or directory
15 | #include <cpuid.h>
| ^~~~~~~~~

kernel and headers version: 6.0.9; ubuntu 22.04. Incase its pertinent- I am using 3.10 version of python.

Confusion about the paper "Hide and Seek with Spectres"

Hi, Sorry to contact you in this way, but I failed to find your email address.

I am reading your paper "Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing". When reading the right side of page 7, I have an incomprehension regarding the value of i'. In order to generate Contract(p, i) = Contract(p, i′ ), I think i' should be {rax=20, rbx=70} rather than {rax=10, rbx=70}.

When i={rax=20,rbx=5} and i'={rax=20, rbx=70}, it can successfully produce Contract(p, i) = Contract(p, i′) and Measure(p, i, µ) != Measure(p, i′, µ).

I'm not sure if my understanding is correct. Can you help clarify my doubt? Thanks a lot.

x86/generator: Could not find an instruction to patch flags

I tried fuzzing using this configuration file:

supported_categories:
  - BASE-COND_BR
  - BASE-BITBYTE
  - BASE-CMOV
  - BASE-FLAGOP
  - BASE-LOGICAL

contract_observation_clause: ct
contract_execution_clause:
   - seq

min_bb_per_function: 2
max_bb_per_function: 2
test_case_size: 24
avg_mem_accesses: 12
program_generator_seed: 0
input_gen_entropy_bits: 16
memory_access_zeroed_bits: 0

and this command:

./cli.py fuzz -s x86/isa_spec/base.json -i 35 -n 500 -c tests/

After a few hunters of rounds, I encounter this exception. Every time it happens in a different round.

generator.GeneratorException: Could not find an instruction to patch flags ['OF'] , when OF modification in the supported instructions

The instructions I enable implicitly set the OF flag, but still this exception is raised.

Bug: Acceptance test "#PF-smap speculation" fails on Linux with SMAP disabled

Acceptance test "#PF-smap speculation" fails on Linux with SMAP disabled

How to reproduce:

• Boot Linux with nosmap
• Build kernel module (version 1.3.1)
• Run ./tests/x86_tests/acceptance.bats -f "smap"

Syntax error in demo yamls (Actors)

demo/detecting-mds.yaml and demo/detecting-foreshadow.yaml have this structure:

# environment
actor:
  - name: "main"
  - data_properties:
    - accessed: False

When then should have this structure:

# Actors
actors:
  - main:
    - data_properties:
      - present: true

Some confusion about the paper

Find "Downfall" Attacks with Revizor?

Hi!
We're two cyber security students from Lübeck, Germany. We're currently working on a group project regarding Revizor and are seeking information from you, the experts :)
We've managed to reproduce your findings regarding Spectre, SCO and ZDI, which was already one of our project goals. We're now looking into the Downfall Attacks (https://downfall.page/media/downfall.pdf) and would like to see if we can maybe reproduce them using Revizor. As far as we understand, we would need to add support for the "gather" vector instruction to Revizor.
Now our humble questions before we start running:
Do you see any possibility to support fuzzing the given instruction(s) with Revizor? Could you give us a hint on how to add the instructions to the ISA information file, maybe adding a whole new contract for the vector instructions?

It would be very kind of you if you could give us pointers on where to start here.

Thank you!

Merlin + Lennart

ERROR: Unknown configuration variable enable_faulty_page. [in big-fuzz.yaml]

ERROR: Unknown configuration variable enable_faulty_page.
It's likely a typo in the configuration file.

Error minimizing test cases: Fences

I encountered what I believe to be unexpected behaviour when running the minimizing function with --add-fences enabled:

(1) I got a random generated x86 program from Revizor using a relatively basic configuration
(2) I tried executing the minimize function on the program (minasms/3f.asm) via the following line:
./cli.py minimize -s x86/isa_spec/base.json -c example-config.yaml -i minasms/3.asm -o minasms/3f.asm -n 100 --add-fences
- This failed, giving the following error message: "generator.AsmParserException: Could not parse line 10
Reason: Terminator not at the end of BB"
(3) I then minimized this program (into minasms/min3.asm, without adding fences) and tried adding fences to that minimized version
with the following line:
./cli.py minimize -s x86/isa_spec/base.json -c example-config.yaml -i minasms/min3.asm -o minasms/min3f.asm -n 100 --add-fences
- This failed too, giving the same error message as the one in (2).

There errors were encountered on the 24th of February, with hyperthreading disabled and the latest version of Revizor to that date. The files were later re-fuzzed again in case of false positives, but both files when fuzzed still presented a violation.
I've left a .zip with the two .asm files and the .yaml file which triggered the error. The original test case file was generated with the same configuration as the one used to try to add fences.

cant-fence.zip

Fuzzing campaign does not exit with timeout flag

Fuzzing campaign does not timeout and exit but continues execution until all test cases are executed. Issue noticed with speculation filter set to true.

Arm Generator creates out of spec loads and stores.

We have seen a couple out of spec instructions generated by the Arm ISA generator. This occurs due to a missing constraint whereby post-indexed or pre-indexed with writeback loads and stores cannot share the same address and src/dest register. For example, the generator will create the instruction str W0,[X0],#-59, which targets R0 for the source of both address and data. This is prohibited according to the Arm developer portal where it states:

Rn must not be the same as Rd, if the instruction:

• is pre-indexed with writeback (the ! suffix)
• is post-indexed
• uses the T suffix.

big-fuzz.yaml doesnt exist

I dont see a file in https://github.com/microsoft/sca-fuzzer/blob/main/src/tests/big-fuzz.yaml. can you verify? You have referenced this file as an example in the documentation.

generator: non-reproducible results when running with multiple permitted_faults

When running an experiment with multiple values in the config option permitted_faults, each test case experiences a randomly-selected fault from the list. The makes violations hard to reproduce (e.g., when running with -t flag) because a different fault will be selected each time the experiment is repeated.

BUG: Incorrect implementation of program_generator_seed

When trying to reproduce a violation via tfuzz, we cannot re-generate the same program using the program_generator_seed parameter in the yaml as intended.

For example, if our violation is found after 4822 test programs, using initial program_generator_seed 830819, then our violation-causing program seed should be 830819 + 4822 = 835641. This appears to work as expected (i.e. if we can actually set the seed to 835641, then we will generate the same violating program).

However, when running tfuzz using the same template, if we want to generate this violating program again, we must run with at least -n 2. If our desired seed is 835641, we must set program_generator_seed: 835640 and use -n 2 to (eventually) generate the program with seed 835641.

If we only use -n 1 and program_generator_seed: 835641, then we will not be able to re-generate the same program, likely instead generating the program at seed 835642.

A secondary request would be to insert the program seed into the "Generation Properties" portion of the output report.txt.
Currently, it only shows the given program seed used when launching Revizor, not the seed used to find the violating test case.
If the initial seed is randomized as is default, then the "Program seed" value will show as 0 when output.

Make a mirror for the x86 ISA spec

Can you verify if you are able to fetch: "https://uops.info/instructions_Jan2022.xml". When I run get_spec.py. I am unable to locate this file.

CPUID cannot be emulated correctly by Unicorn, so it makes the test case behave differently on the model and on the target

This is an unobvious constraint, and we should at add a warning about it in Revizor.

Bug: Ctrl-C causes the fuzzer to store a "bug" violation

Copied from @brianfu's PR:

Using "CTRL+C" to cancel the run halfway will now cause it to spit out a "bug" violation for the canceled run (assuming this is to detect archfuzz bugs). Be careful to distinguish between actual architectural bugs and the false positives that are just testing artifacts.

x86/model: Incorrect handling of string operations in the NullInj contract

String operations can access multiple memory addresses with some of them triggering a fault and some not. Yet the nullinj-fault contract injects zeros into all of the accesses if at least one of them faults. It leads to contract violations, which could be considered a fault positive.

Minimal test case:

.intel_syntax noprefix
MFENCE # instrumentation
.test_case_enter:

AND RDI, 0b1111111111111 # instrumentation
ADD RDI, R14 # instrumentation
AND RSI, 0b1111111111111 # instrumentation
ADD RSI, R14 # instrumentation
AND RCX, 0xff # instrumentation
ADD RCX, 1 # instrumentation
REPNE MOVSW

AND RAX, 0b1111111111111 # instrumentation
MOV rax, qword ptr [R14 + RAX]

.test_case_exit:
MFENCE # instrumentation

Config:

contract_observation_clause: loads+stores+pc
contract_execution_clause:
    - nullinj-fault

input_gen_entropy_bits: 24
memory_access_zeroed_bits: 0
inputs_per_class: 2

permitted_faults:
    - PF-present

logging_modes:
  - info
  - stat
  - dbg_violation

Hardcoded addresses

In templates.c of executor folder exist the following hardcoded addresses
#define TEMPLATE_ENTER 0x0fff379000000000 #define TEMPLATE_INSERT_TC 0x0fff2f9000000000 #define TEMPLATE_RETURN 0x0fff279000000000 #define TEMPLATE_JUMP_EXCEPTION 0x0fff479000000000
and the same can be seen also in the arm port in the same file
#define TEMPLATE_ENTER 0x00001111 #define TEMPLATE_INSERT_TC 0x00002222 #define TEMPLATE_RETURN 0x00003333
It is not documented where this addresses came from,as a result we cant find the equivalent addresses in a potential port

postprocessor: automatic detection of speculation sources

One common step in analyzing a contract violation is to determine which of the instructions in a test case trigger speculation (let's call such instructions "speculation sources"). So far, this analysis has been done manually, as for example described in the Fuzzing Guide (Step 3 in Analyzing The Violation).

This issue is a proposal to automate the task, as follows: Revizor steps through the instruction in the test case and remove them one at a time. In each iteration, Revizor monitors the speculation filter (i.e., monitoring the number of issued and retired uops). If the test case with an instruction removed still triggers speculation, then this instruction is not a speculation source. Otherwise, if speculation disappears, Revizor adds a comment in the corresponding assembly line to indicate this instruction as a speculation source, and (optionally) prints the instruction in the terminal.

Some Python 3.9 functions are used

There are several instances of python 3.9 functions being used when python 3.7 is the minimum listed version. Supporting python 3.7 would be good for lower bar to entry. An example of the 3.9 function use is the removeprefix function.

sca-fuzzer/src/x86/isa_spec/get_spec.py

Lines 117 to 119 in 8bb2efa

	name = name.removeprefix("{load} ")
	name = name.removeprefix("{store} ")
	name = name.removeprefix("{disp32} ")

sca-fuzzer/src/generator.py

Line 135 in 8bb2efa

msg = msg.removeprefix(asm_file + ":")

sca-fuzzer/src/generator.py

Line 223 in 8bb2efa

func_name = label.removeprefix(".function_")

sca-fuzzer/src/generator.py

Line 679 in 8bb2efa

operands_raw = line.removeprefix(name).split(",")

At present, each of these could be replaced with a call to an older set of functions, for example:

if line.startswith(name):
                operands_raw = line[len(name):].split(",")
            else:
                operands_raw = line.split(",")

BUG: rvzr accessing /home/t-oleksenkoo

Followed the steps on README and ran rvzr fuzz command with -c demo/conf-v1.yaml.

Get the following error:
It seems it is trying to access /home/t-oleksenkoo/bin/binutils-gdb/gas/as-new

INFO: [prog_gen] Setting program_generator_seed to random value: 53533
/bin/sh: 1: /home/t-oleksenkoo/bin/binutils-gdb/gas/as-new: not found

Traceback (most recent call last):
File "/root/venv-revizor/bin/rvzr", line 8, in
sys.exit(main())
File "/root/venv-revizor/lib/python3.10/site-packages/revizor/cli.py", line 237, in main
exit_code = fuzzer.start(
File "/root/venv-revizor/lib/python3.10/site-packages/revizor/x86/x86_fuzzer.py", line 80, in start
return super().start(num_test_cases, num_inputs, timeout, nonstop)
File "/root/venv-revizor/lib/python3.10/site-packages/revizor/fuzzer.py", line 93, in start
test_case = self.generator.create_test_case('generated.asm')
File "/root/venv-revizor/lib/python3.10/site-packages/revizor/generator.py", line 135, in create_test_case
self.assemble(asm_file, bin_file)
File "/root/venv-revizor/lib/python3.10/site-packages/revizor/generator.py", line 169, in assemble
raise e
File "/root/venv-revizor/lib/python3.10/site-packages/revizor/generator.py", line 162, in assemble
out = run(f"/home/t-oleksenkoo/bin/binutils-gdb/gas/as-new {asm_file} -o {bin_file}", shell=True, check=True, capture_output=True)
File "/usr/lib/python3.10/subprocess.py", line 526, in run
raise CalledProcessError(retcode, process.args,

build error - At least one file selection option must be defined in the tool.hatch.build.targets.wheel table

when running make install , python3 -m build fails with the following error message:

Unable to determine which files to ship inside the wheel using the following heuristics: https://hatch.pypa.io/latest/plugins/builder/wheel/#default-file-selection

At least one file selection option must be defined in the tool.hatch.build.targets.wheel table, see: https://hatch.pypa.io/latest/config/build/

As an example, if you intend to ship a directory named foo that resides within a src directory located at the root of your project, you can define the following:

[tool.hatch.build.targets.wheel]
packages = ["src/foo"]

can be fixed by adding this to the pyproject.toml file:

    ...
    [tool.hatch.build.targets.wheel] 
    packages = ["revizor"]  

rvzr minimize generate fenced.asm file and may cause confusions

when running rvzr minimize with/without “–add fences” a file fenced.asm is generated. the file includes lfence after every instruction.

this is very confusion, as wehn using “–add fences” you expect to get assembly file with max number of fences that still fails, and you may thing that fenced.asm is the file and not the file name you put under "-o" option of rvzr.

Model traces are printed only for nesting=1

When logging.dbg_model is set and model_max_nesting != 1, the model traces are still printed as if max_nesting = 1.

Cause: In service.py:trc_fuzzer_dump_traces the nesting level is hard-coded to 1. I also found the same bug in service.py:fuzzer_report_violations.

CC: @janahofmann