Maelys DL

Testing


███████╗██╗   ██╗███████╗███████╗
██╔════╝██║   ██║╚══███╔╝╚══███╔╝
█████╗  ██║   ██║  ███╔╝   ███╔╝
██╔══╝  ██║   ██║ ███╔╝   ███╔╝
██║     ╚██████╔╝███████╗███████╗
╚═╝      ╚═════╝ ╚══════╝╚══════╝

Maelys DL fuzzes its Datalog parser with two independent coverage-guided targets. Both targets parse arbitrary byte sequences through the same parser entry point, but use different fuzzing engines. This gives the parser two complementary sources of mutations, coverage feedback, and crash discovery.

The goal is simple: every input must be handled safely. Valid Datalog may parse. Invalid Datalog may be rejected. Random bytes may fail immediately. None of these cases may crash, hang, leak, or trigger undefined behaviour.

libFuzzer

In-process, coverage-guided

libFuzzer runs the parser in-process through LLVMFuzzerTestOneInput. It is fast, easy to run locally, and integrates tightly with AddressSanitizer and UndefinedBehaviorSanitizer. It is the preferred target for quick local parser safety checks.

AFL++

Persistent mode, shared-memory feedback

AFL++ runs a persistent-mode harness around the same parser path. It uses its own mutation strategy and shared-memory coverage feedback. This makes it a useful second opinion: bugs missed by one engine may be found by the other.

What is fuzzed?

Both fuzzers use the same high-level harness. For each generated input, Maelys DL creates a fresh ruleset, installs a small known vocabulary, parses the input, and then clears all parser state.

The main code paths under fuzz are:

lexer             — turns raw bytes into tokens
parser            — parses facts, rules, atoms, variables, and literals
rule-safety check — rejects unsafe variables
stratification    — rejects recursion through negation
comparisons       — parses numeric, boolean, and symbolic filters

The fuzz target does not need the input to be valid. Parser errors are normal and expected. The invariant is that every input must be handled safely.

Accepted outcome:
  ✓ valid program parsed successfully
  ✓ invalid program rejected with a parser/validation error
  ✓ malformed or binary input rejected safely
 
Rejected outcome:
  ✗ crash
  ✗ hang
  ✗ memory leak
  ✗ undefined behaviour
  ✗ sanitizer finding

Why the harness registers atoms. Maelys DL uses an explicit atom vocabulary. If no atoms are registered before parsing, most string constants are rejected immediately as unknown atoms. By registering common atoms such as "alice", "bob", "main", and "push", the fuzzer can reach deeper parser paths such as rule-safety checks, negation, stratification, and comparison filters.

Seed corpus

Both fuzzers start from the same corpus. The corpus contains small Datalog files covering valid programs, invalid programs, regression cases, comparison filters, and malformed byte sequences.

tests/corpus/
  valid/
    minimal_fact.dl          safe("alice").
    rule_with_negation.dl    allow(X) :- user(X), not(blocked(X)).
    recursive_path.dl        path(X,Z) :- path(X,Y), edge(Y,Z).
    comparison_int_gte.dl    allow(X) :- score(X, Level), Level >= 3.
    comparison_eq_symbol.dl  allow(X) :- owns(X, Name), Name = "alice".
    comparison_eq_bool.dl    allow(X) :- score(X, Flag), Flag = true.
    ...
 
  invalid/
    parser/                  parser rejections with expected diagnostics
    lexer/                   invalid UTF-8, oversized tokens
    stratification/          negative cycles
 
  regression/
    previously failing inputs kept as permanent seeds
 
  malformed/
    binary data, truncated rules, null bytes

A good seed corpus is important because coverage-guided fuzzing mutates existing inputs. Starting from realistic Datalog snippets helps the fuzzer quickly reach the interesting parts of the parser instead of spending most of its time on random bytes that fail at the lexer boundary.

Comparison-filter seeds are especially useful. They give the mutation engine valid examples of expressions such as Level >= 3, Name = "alice", or Flag = true. From these seeds the fuzzer can mutate operators, values, variables, and literal order while staying close to syntactically meaningful programs.

Dictionary

Both targets share tests/fuzz/datalog.dict, which seeds the mutation engine with Datalog-specific tokens:

":-"   "."   ","   "("   ")"     ← rule syntax
"not("                            ← negation
"="  "!="  "<"  ">"  "<="  ">="  ← comparison operators
"X"  "Y"  "Z"  "U"  "V"  "_"    ← variables and wildcard
"allow"  "deny"  "safe"  "user"  ← common predicates
"alice"  "bob"  "main"  "push"   ← common atoms

Without a dictionary, the fuzzer would have to discover syntax such as :- or >= by chance. With a dictionary, it quickly produces inputs that look like real Datalog programs and exercises deeper parser paths.

Running libFuzzer

libFuzzer can run locally when the local compiler supports it. It can also run inside Docker for a reproducible Linux environment.

cd extern/maelys-datalog
 
make -f Makefile.fuzz fuzz-clean
make -f Makefile.fuzz fuzz-smoke

Docker Linux run:

cd extern/maelys-datalog
 
ASAN_IMAGE=maelys-datalog-asan-linux:ubuntu24.04
docker run --rm --platform linux/arm64 \
  -v "$(pwd):/src:ro" \
  -w /work \
  "$ASAN_IMAGE" \
  bash -lc 'tar --exclude=.git --exclude=build -C /src -cf - . | tar -xf -; \
            make -f Makefile.fuzz fuzz-clean; \
            make -f Makefile.fuzz fuzz-smoke'

Typical successful output:

INFO: entries found in tests/fuzz/datalog.dict
INFO: files found in build/fuzz/seed
Done 10000 runs
stat::new_units_added: ...
stat::peak_rss_mb:     ...
==> Smoke run PASS

The exact number of discovered units may vary across compiler versions, platforms, and corpus state. The important result is that the run completes without crash, timeout, leak, or sanitizer report.

Running AFL++

AFL++ is best run inside Linux. The harness uses shared-memory coverage feedback, which is not always available from the macOS host kernel.

cd extern/maelys-datalog
 
make -f Makefile.afl afl-smoke-linux

Typical successful output:

Persistent mode binary detected.
Using SHARED MEMORY FUZZING feature.
Dictionary entries loaded.
Seed corpus loaded.
Time limit reached.
Crashes found: 0
Hangs found:   0
==> Smoke run complete

macOS shared-memory limitation. On macOS, AFL++ may fail with a shmat() error. This is a host-kernel limitation, not a parser defect. Use the Docker Linux target for AFL++. libFuzzer does not have this limitation and can usually run natively on macOS.

Interpreting a smoke run

A fuzz smoke is a bounded safety check designed to be fast enough for local development.

Field	Meaning
`new_units_added` / `new corpus items`	Inputs that discovered new edge coverage
`Crashes found: 0`	No crash was observed
`Hangs found: 0`	No timeout was observed
`ASAN/UBSAN findings: none`	No memory or undefined-behaviour issue was reported

A healthy smoke run discovers new coverage from the seed corpus and terminates without sanitizer output. The exact coverage percentage is less important than the safety properties: no crash, no hang, no leak, no undefined behaviour.

Reproducing a crash

If a fuzzer finds a crash or hang, it writes the triggering input to a findings directory.

build/fuzz/findings/default/crashes/   libFuzzer-style findings
build/afl/findings/default/crashes/    AFL++ crashes
build/afl/findings/default/hangs/      AFL++ hangs

Replay a libFuzzer input:

./build/fuzz/fuzz_parse_ruleset path/to/crash_input

Replay an AFL++ input:

./build/afl/fuzz_parse_ruleset_afl < path/to/crash_input

Minimize an AFL++ crash:

afl-tmin \
  -i crash_input \
  -o minimized \
  -- ./build/afl/fuzz_parse_ruleset_afl

When a sanitizer reports a bug, read the first SUMMARY: line and the stack trace. The stack trace points directly to the parser, lexer, registry, or validation function that needs to be fixed.

What fuzzing proves

A smoke run gives evidence that:

  ✓ the parser accepts or rejects arbitrary inputs safely
  ✓ the valid, invalid, regression, and malformed seed corpus does not crash
  ✓ sanitizer-instrumented parser paths do not report memory errors
  ✓ registered atoms let the fuzzer reach deeper validation paths
  ✓ libFuzzer and AFL++ agree on the basic crash-free property

A smoke run does not prove that:

  ✗ every parser path has been exhaustively covered
  ✗ every possible Datalog program has been tested
  ✗ solver output is semantically correct
  ✗ long-running campaigns will find no bugs
  ✗ code outside the parser harness is covered

For deeper assurance, run a longer campaign on a dedicated machine, keep the generated corpus, triage crashes, minimize interesting inputs, and promote useful reproducers into the permanent regression corpus.

File map

tests/fuzz/
  fuzz_parse_ruleset.c        libFuzzer target
  fuzz_parse_ruleset_afl.c    AFL++ persistent-mode target
  datalog.dict                shared Datalog dictionary
 
Makefile.fuzz                 libFuzzer build and smoke targets
Makefile.afl                  AFL++ build, smoke, and Docker targets
 
docker/
  asan-linux/Dockerfile       Linux ASAN/UBSAN environment
  aflpp-linux/Dockerfile      Linux AFL++ environment
 
tests/corpus/
  valid/                      valid Datalog programs
  invalid/                    invalid programs with expected rejection
  regression/                 previously failing inputs
  malformed/                  binary, truncated, and hostile inputs

Where to go next

Rulesets — parser and policy language reference.
Algorithms — evaluation, recursion, stratification, and comparison semantics.

Fuzzing