68 lines
1.5 KiB
Bash
Executable file
68 lines
1.5 KiB
Bash
Executable file
#!/usr/bin/env bash
|
|
# Optional source-confirmation smoke for Fold's KLEE adapter prototype.
|
|
# Skips cleanly when KLEE is not installed.
|
|
set -euo pipefail
|
|
|
|
ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../../.." && pwd)"
|
|
SRC="$ROOT/tests/confirmation/klee/oob_overwrite.c"
|
|
OUT="$ROOT/build/klee-smoke"
|
|
TASK="$OUT/oob_overwrite.task.json"
|
|
RESULT="$OUT/oob_overwrite.result.json"
|
|
|
|
mkdir -p "$OUT"
|
|
cat >"$TASK" <<EOF
|
|
{
|
|
"version": "1",
|
|
"task_id": "klee:oob-overwrite-smoke",
|
|
"finding_id": "oob-access:oob_overwrite.c:10:5",
|
|
"hazard": "oob-access",
|
|
"backend": "source",
|
|
"lane": "clang",
|
|
"adapter": "klee",
|
|
"target": {
|
|
"artifact": "$SRC",
|
|
"function": "vulnerable_copy",
|
|
"source_location": {
|
|
"file": "$SRC",
|
|
"line": 10,
|
|
"column": 5,
|
|
"function": "vulnerable_copy"
|
|
}
|
|
},
|
|
"input_channel": "harness",
|
|
"controlled_values": ["idx"],
|
|
"path_predicate": "idx >= 8 && idx < 16",
|
|
"expected_violation": "out-of-bounds write",
|
|
"artifacts": [],
|
|
"partial": false
|
|
}
|
|
EOF
|
|
|
|
CLANG="${CLANG:-clang}"
|
|
python3 "$ROOT/tests/confirmation/klee/klee_confirm.py" \
|
|
--task "$TASK" \
|
|
--output "$RESULT" \
|
|
--work-dir "$OUT" \
|
|
--clang "$CLANG"
|
|
|
|
STATUS="$(
|
|
python3 - <<PY
|
|
import json
|
|
from pathlib import Path
|
|
print(json.loads(Path('$RESULT').read_text()).get('status', ''))
|
|
PY
|
|
)"
|
|
|
|
case "$STATUS" in
|
|
confirmed)
|
|
echo "ok: KLEE confirmed smoke task"
|
|
;;
|
|
unsupported)
|
|
echo "skip: KLEE adapter unsupported in this environment"
|
|
;;
|
|
*)
|
|
echo "fail: unexpected KLEE smoke status: $STATUS"
|
|
cat "$RESULT"
|
|
exit 1
|
|
;;
|
|
esac
|