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.

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

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.

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.

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

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

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

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.

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

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

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.

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

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

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.

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.

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.

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.

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

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.

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.