-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathMakefile
More file actions
415 lines (371 loc) ยท 17.4 KB
/
Makefile
File metadata and controls
415 lines (371 loc) ยท 17.4 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
# ๐ฑ Meow Decoder - Makefile
.PHONY: help install dev test test-rust test-rust-coverage lint format clean build publish \
formal-proverif formal-proverif-html formal-tla formal-tla-fountain formal-tla-streaming \
formal-tamarin formal-tamarin-duress formal-tamarin-pq formal-tamarin-docker \
formal-verus formal-verus-docker formal-lean formal-lean-sorry formal-all formal-ci \
formal-negative-tla formal-negative-proverif formal-negative-tamarin formal-negative \
verify check-wasm-deps build-wasm build-wasm-release build-wasm-pq build-wasm-node meow-build
help:
@echo "๐ฑ Meow Decoder - Available Commands:"
@echo ""
@echo " make install - Install dependencies"
@echo " make dev - Install dev dependencies"
@echo " make test - Run Python tests"
@echo " make test-rust - Run Rust tests (no coverage)"
@echo " make lint - Lint code"
@echo " make format - Format code"
@echo " make clean - Clean build artifacts"
@echo " make build - Build package"
@echo " make publish - Publish to PyPI"
@echo ""
@echo "๐ Coverage (Codecov monitors Rust only):"
@echo " make test-rust-coverage - Rust coverage via cargo-tarpaulin"
@echo " make test-security - Python security coverage (local gate)"
@echo ""
@echo "๐ฆ Build Targets:"
@echo " make build - Build Python package"
@echo " make build-rust - Build Rust crypto_core"
@echo " make build-wasm - Build WASM bindings (dev)"
@echo " make build-wasm-release - Build optimized WASM"
@echo " make build-wasm-pq - Build WASM with Post-Quantum ML-KEM-1024"
@echo " make meow-build - Build WASM + start browser demo server"
@echo " make prepare-deploy - Prepare WASM demo for hosting"
@echo ""
@echo "๐ Security:"
@echo " make security-test - Run security test suite"
@echo " make sidechannel-test - Run side-channel tests"
@echo " make supply-chain-audit - Run supply-chain audit"
@echo " make stealth-build - Build stealth distribution"
@echo ""
@echo "๏ฟฝ๐ฌ Formal Verification:"
@echo " make formal-proverif - Run ProVerif symbolic model"
@echo " make formal-proverif-html - ProVerif HTML report"
@echo " make formal-tla - Run TLA+ main model (MeowEncode)"
@echo " make formal-tla-fountain - Run TLA+ fountain model (MeowFountain)"
@echo " make formal-tla-streaming - Run TLA+ streaming model (MeowStreaming)"
@echo " make formal-tamarin - Run Tamarin basic equivalence"
@echo " make formal-tamarin-duress - Run Tamarin duress OE (diff mode)"
@echo " make formal-tamarin-pq - Run Tamarin MEOW4 PQ duress OE"
@echo " make formal-tamarin-docker - Run Tamarin via Docker (no native Maude)"
@echo " make formal-negative-tamarin-pq - Run Tamarin PQ negative tests (should FAIL)"
@echo " make formal-negative-tamarin-docker - Run Tamarin PQ negative tests via Docker"
@echo " make formal-verus - Run Verus proofs"
@echo " make formal-verus-docker - Run Verus via Docker (nightly toolchain)"
@echo " make formal-lean - Build Lean 4 proofs"
@echo " make formal-lean-sorry - Check for unapproved sorry"
@echo " make formal-all - Run all formal checks"
@echo " make formal-ci - CI gate (skips unavailable tools)"
@echo " make verify - Run full verification suite"
@echo ""
@echo "๐พ Strong cat passwords only! ๐บ"
install:
pip install -r requirements.txt
dev:
pip install -r requirements.txt
pip install -r requirements-dev.txt
pre-commit install
test:
pytest tests/ -v --cov=meow_decoder
test-security:
@echo "๐พ Running security coverage gate (TIER 1 modules, โฅ85% required)..."
MEOW_TEST_MODE=1 pytest tests/ -v -m "security or crypto or adversarial" \
--cov --cov-config=.coveragerc-security --cov-fail-under=85 \
--cov-report=term-missing --cov-report=xml:coverage-security.xml
lint:
flake8 meow_decoder/
black --check meow_decoder/
mypy meow_decoder/
bandit -r meow_decoder/ -ll
format:
black meow_decoder/ tests/
clean:
rm -f tests/test_e2e.py
rm -rf build/ dist/ *.egg-info
rm -rf .pytest_cache .coverage htmlcov
find . -type d -name __pycache__ -exec rm -rf {} +
find . -type f -name '*.pyc' -delete
build: clean
python -m build
publish: build
twine check dist/*
twine upload dist/*
formal-proverif:
@echo "๐ต Running ProVerif symbolic analysis..."
cd formal/proverif && eval $(opam env) && proverif meow_encode.pv
formal-proverif-html:
@echo "๐ต Generating ProVerif HTML report..."
cd formal/proverif && eval $(opam env) && proverif -html output meow_encode.pv
formal-tla:
@echo "๐ Running TLA+ main model (MeowEncode.tla)..."
cd formal/tla && tlc -config MeowEncode.cfg MeowEncode.tla
formal-tla-fountain:
@echo "๐ Running TLA+ fountain model (MeowFountain.tla)..."
cd formal/tla && tlc -config MeowFountain.cfg MeowFountain.tla
formal-tla-streaming:
@echo "๐ Running TLA+ streaming model (MeowStreaming.tla)..."
cd formal/tla && tlc -config MeowStreaming.cfg MeowStreaming.tla
formal-tamarin:
@echo "๐ฃ Running Tamarin basic equivalence..."
cd formal/tamarin && bash ./run.sh
formal-tamarin-duress:
@echo "๐ฃ Running Tamarin duress observational equivalence (diff mode)..."
cd formal/tamarin && tamarin-prover --diff MeowDuressEquiv.spthy --prove
formal-tamarin-pq:
@echo "๐ฃ Running Tamarin MEOW4 PQ duress OE (diff mode)..."
cd formal/tamarin && tamarin-prover --diff MeowDuressEquivPQ.spthy --prove
formal-tamarin-docker:
@echo "๐ฃ Running Tamarin duress OE via Docker (MEOW3 + MEOW4)..."
docker build -f formal/Dockerfile.tamarin -t meow-tamarin . \
&& docker run --rm meow-tamarin
formal-verus:
@echo "๐ข Running Verus implementation proofs..."
cd crypto_core && verus src/lib.rs
formal-verus-docker:
@echo "๐ข Running Verus proofs via Docker (nightly)..."
docker build -f formal/Dockerfile.verus -t meow-verus . \
&& docker run --rm meow-verus
formal-lean:
@echo "๐ท Building Lean 4 fountain code proofs..."
cd formal/lean && lake build
formal-lean-sorry:
@echo "๐ท Checking for unapproved sorry in Lean files..."
@# NOTE: grep -n output has format "file:N:content"; use ':[[:blank:]]*--'
@# instead of '^[[:blank:]]*--' to correctly skip line/block-comment lines.
@# The -i flag makes the approved-word filters case-insensitive.
@SORRY_COUNT=$$(grep -rn '\bsorry\b' formal/lean/ --include='*.lean' \
--exclude-dir='.lake' --exclude-dir='lake-packages' \
| grep -v -e 'AXIOM:' -e 'APPROVED:' -e ':[[:blank:]]*--' -e ':[[:blank:]]*/--' \
| grep -v -i -e '`sorry`' -e 'sorry instance' -e 'sorry statement' \
-e 'sorry tag' -e 'approved sorry' -e 'sorry for' \
| wc -l); \
if [ "$$SORRY_COUNT" -gt 0 ]; then \
echo "โ Found $$SORRY_COUNT unapproved sorry statement(s):"; \
grep -rn '\bsorry\b' formal/lean/ --include='*.lean' \
--exclude-dir='.lake' --exclude-dir='lake-packages' \
| grep -v -e 'AXIOM:' -e 'APPROVED:' -e ':[[:blank:]]*--' -e ':[[:blank:]]*/--' \
| grep -v -i -e '`sorry`' -e 'sorry instance' -e 'sorry statement' \
-e 'sorry tag' -e 'approved sorry' -e 'sorry for'; \
exit 1; \
else \
echo "โ
No unapproved sorry statements found."; \
fi
# Negative tests: variants that should FAIL (verify positive models are correct)
formal-negative-tamarin-pq:
@echo "๐ด Running Tamarin PQ NEGATIVE tests (should FAIL)..."
@echo "Test 1: KEM ct not bound to HMAC โ diff-equivalence should FAIL"
@cd formal/tamarin && tamarin-prover --diff MeowDuressEquivPQ_NEGATIVE_NoKEMBinding.spthy --prove || echo "โ
Test 1 failed as expected"
@echo "Test 2: Non-uniform failure observables โ PQ_Failure_Uniform_Observable should FAIL"
@cd formal/tamarin && tamarin-prover --diff MeowDuressEquivPQ_NEGATIVE_LeaksFailureReason.spthy --prove || echo "โ
Test 2 failed as expected"
formal-negative-tamarin-docker:
@echo "๐ด Running Tamarin PQ NEGATIVE tests via Docker..."
docker run --rm meow-tamarin bash -c "\
tamarin-prover --diff /formal/tamarin/MeowDuressEquivPQ_NEGATIVE_NoKEMBinding.spthy --prove || echo 'โ
Test 1 failed as expected'; \
tamarin-prover --diff /formal/tamarin/MeowDuressEquivPQ_NEGATIVE_LeaksFailureReason.spthy --prove || echo 'โ
Test 2 failed as expected'"
formal-all: formal-proverif formal-tla formal-tla-fountain formal-tla-streaming formal-tamarin-duress formal-verus formal-lean
@echo ""
@echo "โ
All formal verification complete!"
@echo "๐ See docs/formal_coverage.md for coverage matrix"
\# CI-friendly target: runs available tools, skips missing ones, fails on errors
formal-ci:
@echo "๐ฌ Running CI formal verification gates..."
@FAIL=0; \
if command -v proverif >/dev/null 2>&1; then \
echo "โโ ProVerif โโ"; \
$(MAKE) formal-proverif || FAIL=1; \
else echo "โญ๏ธ ProVerif not available, skipping"; fi; \
if command -v tlc >/dev/null 2>&1 || (command -v java >/dev/null 2>&1 && [ -f ~/tla/tla2tools.jar ]); then \
echo "โโ TLA+ (MeowEncode) โโ"; \
$(MAKE) formal-tla || FAIL=1; \
echo "โโ TLA+ (MeowFountain) โโ"; \
$(MAKE) formal-tla-fountain || FAIL=1; \
echo "โโ TLA+ (MeowStreaming) โโ"; \
$(MAKE) formal-tla-streaming || FAIL=1; \
else echo "โญ๏ธ TLA+ (java) not available, skipping"; fi; \
if command -v tamarin-prover >/dev/null 2>&1; then \
echo "โโ Tamarin (native) โโ"; \
$(MAKE) formal-tamarin-duress || FAIL=1; \
elif command -v docker >/dev/null 2>&1; then \
echo "โโ Tamarin (Docker) โโ"; \
$(MAKE) formal-tamarin-docker || FAIL=1; \
else echo "โญ๏ธ Tamarin not available (no native or Docker), skipping"; fi; \
if command -v verus >/dev/null 2>&1; then \
echo "โโ Verus (native) โโ"; \
$(MAKE) formal-verus || FAIL=1; \
elif command -v docker >/dev/null 2>&1; then \
echo "โโ Verus (Docker, nightly) โโ"; \
$(MAKE) formal-verus-docker || FAIL=1; \
else echo "โญ๏ธ Verus not available (no native or Docker), skipping"; fi; \
if command -v lake >/dev/null 2>&1; then \
echo "โโ Lean 4 โโ"; \
$(MAKE) formal-lean || FAIL=1; \
echo "โโ Lean sorry gate โโ"; \
$(MAKE) formal-lean-sorry || FAIL=1; \
else echo "โญ๏ธ Lean not available, skipping"; fi; \
if [ "$$FAIL" -ne 0 ]; then \
echo "โ Formal verification FAILED"; exit 1; \
else \
echo "โ
All available formal checks passed!"; \
fi
verify:
bash ./scripts/verify_all.sh
# ๐ฅท Stealth build for deniability
stealth-build:
@echo "๐ฅท Building stealth distribution..."
python scripts/stealth_build.py
@echo "โ
Stealth build created in dist/stealth/"
# ๐ฌ Side-channel tests
sidechannel-test:
@echo "๐ฌ Running side-channel tests..."
pytest tests/test_sidechannel.py -v --tb=short
@echo "โ
Side-channel tests complete"
# ๐ Security-focused tests
security-test:
@echo "๐ Running security test suite..."
pytest tests/test_security.py tests/test_adversarial.py tests/test_sidechannel.py -v --tb=short
@echo "โ
Security tests complete"
# ๐ฆ Supply-chain audit
supply-chain-audit:
@echo "๐ฆ Running supply-chain audit..."
pip-audit
cd crypto_core && cargo audit
cd crypto_core && cargo deny check
@echo "โ
Supply-chain audit complete"
# ๐ฆ Rust crypto_core build
build-rust:
@echo "๐ฆ Building Rust crypto_core..."
cd crypto_core && cargo build --release --features full-software
@echo "โ
Rust build complete"
# ๐ฆ Rust coverage (cargo-tarpaulin) โ this is what Codecov monitors
test-rust-coverage:
@echo "๐ฆ Running Rust coverage (cargo-tarpaulin)..."
@echo "๐ crypto_core coverage:"
cd crypto_core && cargo tarpaulin \
--features "pure-crypto,pq-crypto" \
--out Html --out Lcov \
--output-dir . \
--timeout 300 \
--exclude-files "src/wasm.rs" \
--exclude-files "src/hsm.rs" \
--exclude-files "src/tpm.rs" \
--exclude-files "src/yubikey_piv.rs" \
--exclude-files "src/verus_proofs.rs" \
--exclude-files "src/verus_kdf_proofs.rs"
@echo ""
@echo "๐ rust_crypto coverage:"
cd rust_crypto && cargo tarpaulin \
--lib --tests \
--out Html --out Lcov \
--output-dir . \
--timeout 300 \
--exclude-files "src/lib.rs"
@echo ""
@echo "โ
Rust coverage reports:"
@echo " crypto_core/tarpaulin-report.html"
@echo " rust_crypto/tarpaulin-report.html"
# ๐ฆ Quick Rust test (no coverage instrumentation)
test-rust:
@echo "๐ฆ Running Rust tests..."
cd crypto_core && cargo test --features "pure-crypto,pq-crypto"
cd rust_crypto && cargo test --features "pq"
@echo "โ
Rust tests complete"
# ๐ WASM build (development)
build-wasm: check-wasm-deps
@echo "๐ Building WASM bindings (development)..."
cd crypto_core && wasm-pack build --target web --dev --features wasm
@echo "โ
WASM development build complete in crypto_core/pkg/"
# ๐ง Check and install WASM dependencies
check-wasm-deps:
@echo "๐ Checking WASM build dependencies..."
@if ! command -v cargo >/dev/null 2>&1; then \
echo "๐ฆ Rust/Cargo not found. Installing..."; \
if command -v apk >/dev/null 2>&1; then \
echo " Detected Alpine Linux - using apk"; \
sudo apk add --no-cache rust cargo wasm-pack 2>/dev/null || apk add --no-cache rust cargo wasm-pack; \
elif command -v apt-get >/dev/null 2>&1; then \
echo " Detected Debian/Ubuntu - using apt"; \
sudo apt-get update && sudo apt-get install -y rustc cargo; \
cargo install wasm-pack; \
elif command -v brew >/dev/null 2>&1; then \
echo " Detected macOS - using Homebrew"; \
brew install rust wasm-pack; \
else \
echo "โ Could not detect package manager. Please install Rust manually:"; \
echo " curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh"; \
echo " cargo install wasm-pack"; \
exit 1; \
fi; \
fi
@if ! command -v wasm-pack >/dev/null 2>&1; then \
echo "๐ฆ wasm-pack not found. Installing..."; \
if command -v apk >/dev/null 2>&1; then \
sudo apk add --no-cache wasm-pack 2>/dev/null || apk add --no-cache wasm-pack; \
else \
cargo install wasm-pack; \
fi; \
fi
@echo "โ
Dependencies ready"
# ๐ WASM build (production - optimized)
build-wasm-release: check-wasm-deps
@echo "๐ Building WASM bindings (production - optimized)..."
cd crypto_core && wasm-pack build --target web --release --features wasm
@echo "๐ง Running wasm-opt for additional optimization..."
@if command -v wasm-opt >/dev/null 2>&1; then \
wasm-opt -O3 --strip-debug crypto_core/pkg/crypto_core_bg.wasm -o crypto_core/pkg/crypto_core_bg.wasm; \
echo "โ
wasm-opt optimization complete"; \
else \
echo "โ ๏ธ wasm-opt not found (optional). Install with: cargo install wasm-opt"; \
echo " Skipping additional optimization..."; \
fi
@echo "โ
WASM production build complete in crypto_core/pkg/"
@echo "๐ Package size: $$(du -h crypto_core/pkg/*.wasm | cut -f1)"
# ๐ฎ WASM build with Post-Quantum ML-KEM-1024 support
build-wasm-pq: check-wasm-deps
@echo "๐ฎ Building WASM with Post-Quantum ML-KEM-1024 support..."
cd crypto_core && wasm-pack build --target web --release --features wasm-pq
@echo "๐ง Running wasm-opt for additional optimization..."
@if command -v wasm-opt >/dev/null 2>&1; then \
wasm-opt -O3 --strip-debug crypto_core/pkg/crypto_core_bg.wasm -o crypto_core/pkg/crypto_core_bg.wasm; \
echo "โ
wasm-opt optimization complete"; \
else \
echo "โ ๏ธ wasm-opt not found (optional). Install with: cargo install wasm-opt"; \
echo " Skipping additional optimization..."; \
fi
@echo "โ
WASM Post-Quantum build complete in crypto_core/pkg/"
@echo "๐ Package size: $$(du -h crypto_core/pkg/*.wasm | cut -f1)"
@echo ""
@echo "๐ฎ Post-Quantum features enabled:"
@echo " - ML-KEM-1024 (Kyber) quantum-resistant key exchange (experimental)"
@echo " - Hybrid X25519 + ML-KEM mode"
@echo " - Targets NIST PQ Level 5 (not externally audited)"
# ๐ WASM Node.js build (for server-side use)
build-wasm-node: check-wasm-deps
@echo "๐ Building WASM bindings for Node.js..."
cd crypto_core && wasm-pack build --target nodejs --release --features wasm
@echo "โ
WASM Node.js build complete in crypto_core/pkg/"
# ๐ฑ meow-build - Build WASM + start HTTP server
meow-build: build-wasm
@echo ""
@echo "โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ"
@echo "๐ฑ Meow Decoder Demo Server"
@echo "โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ"
@echo ""
@echo "๐ Local URL: http://localhost:8080/examples/wasm_browser_example.html"
@echo ""
@echo "๐ก In Codespaces/Dev Containers:"
@echo " 1. Open the 'Ports' tab in the bottom panel"
@echo " 2. Forward port 8080 (right-click โ Forward Port)"
@echo " 3. Click the forwarded URL + append /examples/wasm_browser_example.html"
@echo ""
@echo "โ ๏ธ Port 8080 is NOT auto-forwarded by default (for privacy)."
@echo " You must manually forward it to access the demo."
@echo ""
@echo "Press Ctrl+C to stop the server"
@echo "โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ"
@echo ""
python3 -m http.server 8080
# ๐ฆ Prepare WASM demo for deployment (PythonAnywhere, etc.)
prepare-deploy:
@echo "๐ฆ Preparing WASM demo for deployment..."
@./scripts/prepare_pythonanywhere.sh
@echo "๐ See examples/PYTHONANYWHERE_HOSTING.md for hosting instructions"
.DEFAULT_GOAL := help