Skip to content

Commit 1ae87cd

Browse files
avrabeavrabe
committed
feat(architecture): implement mixed std/no_std environment with safety-critical separation
This commit establishes a foundational architectural separation between safety-critical core components and system integration layers to support both ASIL-compliant embedded deployments and full-featured server environments. ## Core Architecture Changes **Safety-Critical Core Layer (no_std + no_alloc by default):** - wrt-foundation, wrt-runtime, wrt-decoder, wrt-format, wrt-instructions - wrt-error, wrt-sync, wrt-math, wrt-intercept, wrt-component - Default to pure no_std with bounded collections and static memory allocation - Panic handler conflicts resolved through proper dependency separation **System Integration Layer (std when needed):** - wrtd, wrt-wasi, wrt-host, wrt-platform, wrt-logging, wrt-debug - Can use dynamic allocation for I/O, networking, and external resources - Bridge to core layer through memory boundary enforcement ## Key Fixes **Dependency Management:** - Fixed circular dependencies causing panic handler conflicts - Made wrt-platform and wrt-host optional in wrt-runtime - Proper default-features = false propagation across workspace **Conditional Compilation:** - Platform-dependent modules (atomic ops, threading) properly feature-gated - Vec/String usage conditional on alloc feature - Import conflicts resolved between std and no_std environments **Memory Boundary Enforcement:** - Leverages existing hierarchical budget system - Data exchange through bounded collections with capacity limits - Clear separation prevents std from contaminating safety-critical paths ## Build Matrix Support Core components now build successfully with: - `cargo build -p wrt --no-default-features` (pure no_std + no_alloc) - `cargo build -p wrt --no-default-features --features alloc` (no_std + bounded alloc) - `cargo build -p wrt --features std` (full std with integration layer) ## Documentation & Tooling - Added comprehensive mixed environment architecture documentation - Enhanced CI workflows with Kani verification and security audits - Build verification matrix for testing all deployment configurations - Feature standardization across workspace with safety tier compliance This foundation enables deterministic ASIL-D compliance in core components while maintaining flexibility for system integration and development tooling. BREAKING CHANGE: Default build mode changed from std to no_std for core crates. Use explicit --features std for integration layer functionality.
1 parent ccc53bb commit 1ae87cd

File tree

271 files changed

+21235
-2997
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

271 files changed

+21235
-2997
lines changed

‎.github/kani-badge.json‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
{
2+
"schemaVersion": 1,
3+
"label": "formal verification",
4+
"message": "KANI",
5+
"color": "brightgreen",
6+
"namedLogo": "rust",
7+
"logoColor": "white",
8+
"style": "for-the-badge",
9+
"cacheSeconds": 86400
10+
}

‎.github/workflows/kani-verification.yml‎

Lines changed: 293 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,293 @@
1+
name: Formal Verification with KANI
2+
3+
on:
4+
push:
5+
branches: [ main, develop ]
6+
paths:
7+
- '**.rs'
8+
- '**/Cargo.toml'
9+
- '**/Kani.toml'
10+
- '.github/workflows/kani-verification.yml'
11+
pull_request:
12+
branches: [ main, develop ]
13+
paths:
14+
- '**.rs'
15+
- '**/Cargo.toml'
16+
- '**/Kani.toml'
17+
- '.github/workflows/kani-verification.yml'
18+
schedule:
19+
# Run weekly verification on Sunday at 2 AM UTC
20+
- cron: '0 2 * * 0'
21+
workflow_dispatch:
22+
inputs:
23+
asil_level:
24+
description: 'ASIL verification level'
25+
required: true
26+
default: 'asil-c'
27+
type: choice
28+
options:
29+
- asil-a
30+
- asil-b
31+
- asil-c
32+
- asil-d
33+
package:
34+
description: 'Specific package to verify (optional)'
35+
required: false
36+
default: ''
37+
38+
env:
39+
RUST_BACKTRACE: 1
40+
CARGO_TERM_COLOR: always
41+
KANI_VERSION: '0.54.0'
42+
43+
jobs:
44+
# Quick verification for all PRs
45+
quick-verification:
46+
name: Quick Verification (ASIL-A)
47+
runs-on: ubuntu-latest
48+
if: github.event_name == 'pull_request'
49+
steps:
50+
- uses: actions/checkout@v4
51+
52+
- name: Install Rust
53+
uses: dtolnay/rust-toolchain@stable
54+
with:
55+
toolchain: nightly-2024-01-01
56+
components: rust-src
57+
58+
- name: Cache Cargo
59+
uses: actions/cache@v4
60+
with:
61+
path: |
62+
~/.cargo/bin/
63+
~/.cargo/registry/index/
64+
~/.cargo/registry/cache/
65+
~/.cargo/git/db/
66+
target/
67+
key: ${{ runner.os }}-cargo-kani-${{ hashFiles('**/Cargo.lock') }}
68+
69+
- name: Install KANI
70+
run: |
71+
if ! command -v kani &> /dev/null; then
72+
cargo install --version ${KANI_VERSION} --locked kani-verifier
73+
cargo kani setup
74+
fi
75+
76+
- name: Run Quick Verification
77+
run: |
78+
./scripts/kani-verify.sh --profile asil-a --package wrt-integration-tests
79+
continue-on-error: true
80+
81+
- name: Upload Quick Report
82+
uses: actions/upload-artifact@v4
83+
if: always()
84+
with:
85+
name: kani-quick-report
86+
path: target/kani-reports/verification_report_*.md
87+
88+
# Matrix verification for different ASIL levels and packages
89+
matrix-verification:
90+
name: Verify ${{ matrix.package }} @ ${{ matrix.asil }}
91+
runs-on: ubuntu-latest
92+
if: github.event_name != 'pull_request' || github.event.pull_request.draft == false
93+
strategy:
94+
fail-fast: false
95+
matrix:
96+
asil: [asil-b, asil-c]
97+
package:
98+
- wrt-foundation
99+
- wrt-component
100+
- wrt-sync
101+
- wrt-integration-tests
102+
include:
103+
# Add ASIL-D verification for critical packages only
104+
- asil: asil-d
105+
package: wrt-integration-tests
106+
- asil: asil-d
107+
package: wrt-foundation
108+
109+
steps:
110+
- uses: actions/checkout@v4
111+
112+
- name: Install Rust
113+
uses: dtolnay/rust-toolchain@stable
114+
with:
115+
toolchain: nightly-2024-01-01
116+
components: rust-src
117+
118+
- name: Cache Cargo
119+
uses: actions/cache@v4
120+
with:
121+
path: |
122+
~/.cargo/bin/
123+
~/.cargo/registry/index/
124+
~/.cargo/registry/cache/
125+
~/.cargo/git/db/
126+
target/
127+
key: ${{ runner.os }}-cargo-kani-${{ matrix.package }}-${{ hashFiles('**/Cargo.lock') }}
128+
129+
- name: Install KANI
130+
run: |
131+
if ! command -v kani &> /dev/null; then
132+
cargo install --version ${KANI_VERSION} --locked kani-verifier
133+
cargo kani setup
134+
fi
135+
136+
- name: Run Verification
137+
run: |
138+
./scripts/kani-verify.sh --profile ${{ matrix.asil }} --package ${{ matrix.package }}
139+
timeout-minutes: 30
140+
141+
- name: Upload Verification Report
142+
uses: actions/upload-artifact@v4
143+
if: always()
144+
with:
145+
name: kani-report-${{ matrix.package }}-${{ matrix.asil }}
146+
path: target/kani-reports/
147+
148+
- name: Check for Failures
149+
if: failure()
150+
run: |
151+
echo "::error::Formal verification failed for ${{ matrix.package }} at ${{ matrix.asil }} level"
152+
cat target/kani-reports/verification_report_*.md
153+
154+
# Comprehensive verification for main branch
155+
comprehensive-verification:
156+
name: Comprehensive Verification (All Packages)
157+
runs-on: ubuntu-latest
158+
if: github.ref == 'refs/heads/main' || github.event_name == 'schedule'
159+
steps:
160+
- uses: actions/checkout@v4
161+
162+
- name: Install Rust
163+
uses: dtolnay/rust-toolchain@stable
164+
with:
165+
toolchain: nightly-2024-01-01
166+
components: rust-src
167+
168+
- name: Cache Cargo
169+
uses: actions/cache@v4
170+
with:
171+
path: |
172+
~/.cargo/bin/
173+
~/.cargo/registry/index/
174+
~/.cargo/registry/cache/
175+
~/.cargo/git/db/
176+
target/
177+
key: ${{ runner.os }}-cargo-kani-comprehensive-${{ hashFiles('**/Cargo.lock') }}
178+
179+
- name: Install KANI
180+
run: |
181+
cargo install --version ${KANI_VERSION} --locked kani-verifier
182+
cargo kani setup
183+
184+
- name: Run Comprehensive Verification
185+
run: |
186+
ASIL_LEVEL="${{ github.event.inputs.asil_level || 'asil-c' }}"
187+
PACKAGE="${{ github.event.inputs.package || '' }}"
188+
189+
if [ -n "$PACKAGE" ]; then
190+
./scripts/kani-verify.sh --profile $ASIL_LEVEL --package $PACKAGE --verbose
191+
else
192+
./scripts/kani-verify.sh --profile $ASIL_LEVEL --verbose
193+
fi
194+
timeout-minutes: 60
195+
196+
- name: Generate Coverage Report
197+
if: github.event.inputs.asil_level == 'asil-d' || github.event_name == 'schedule'
198+
run: |
199+
echo "## Coverage Report" >> target/kani-reports/coverage_summary.md
200+
echo "" >> target/kani-reports/coverage_summary.md
201+
if [ -f target/kani-reports/coverage_*.txt ]; then
202+
cat target/kani-reports/coverage_*.txt >> target/kani-reports/coverage_summary.md
203+
else
204+
echo "No coverage data available" >> target/kani-reports/coverage_summary.md
205+
fi
206+
continue-on-error: true
207+
208+
- name: Upload Comprehensive Report
209+
uses: actions/upload-artifact@v4
210+
if: always()
211+
with:
212+
name: kani-comprehensive-report
213+
path: target/kani-reports/
214+
215+
- name: Comment PR with Results
216+
if: github.event_name == 'pull_request'
217+
uses: actions/github-script@v7
218+
with:
219+
script: |
220+
const fs = require('fs');
221+
const reportPath = 'target/kani-reports/verification_report_*.md';
222+
const reports = require('glob').sync(reportPath);
223+
224+
if (reports.length > 0) {
225+
const content = fs.readFileSync(reports[0], 'utf8');
226+
227+
// Extract summary
228+
const summaryMatch = content.match(/## Summary[\s\S]*?##/);
229+
const summary = summaryMatch ? summaryMatch[0] : 'Verification completed.';
230+
231+
github.rest.issues.createComment({
232+
issue_number: context.issue.number,
233+
owner: context.repo.owner,
234+
repo: context.repo.repo,
235+
body: `## 🔍 KANI Formal Verification Results\n\n${summary}\n\n[Full Report](https://github.com/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId})`
236+
});
237+
}
238+
239+
# Summary job to ensure all verifications passed
240+
verification-summary:
241+
name: Verification Summary
242+
runs-on: ubuntu-latest
243+
needs: [quick-verification, matrix-verification]
244+
if: always()
245+
steps:
246+
- name: Check Verification Results
247+
run: |
248+
if [ "${{ needs.quick-verification.result }}" == "failure" ] ||
249+
[ "${{ needs.matrix-verification.result }}" == "failure" ]; then
250+
echo "::error::One or more verification jobs failed"
251+
exit 1
252+
fi
253+
echo "✅ All verification jobs completed successfully"
254+
255+
- name: Download All Reports
256+
uses: actions/download-artifact@v4
257+
with:
258+
pattern: kani-report-*
259+
merge-multiple: true
260+
261+
- name: Generate Summary Report
262+
run: |
263+
echo "# KANI Verification Summary" > summary.md
264+
echo "" >> summary.md
265+
echo "**Date**: $(date)" >> summary.md
266+
echo "**Commit**: ${{ github.sha }}" >> summary.md
267+
echo "" >> summary.md
268+
269+
# Count successes and failures
270+
TOTAL=$(find . -name "verification_report_*.md" | wc -l)
271+
PASSED=$(grep -l "✅ PASSED" verification_report_*.md 2>/dev/null | wc -l || echo 0)
272+
FAILED=$((TOTAL - PASSED))
273+
274+
echo "## Results" >> summary.md
275+
echo "- Total Packages Verified: $TOTAL" >> summary.md
276+
echo "- Passed: $PASSED" >> summary.md
277+
echo "- Failed: $FAILED" >> summary.md
278+
echo "" >> summary.md
279+
280+
if [ $FAILED -gt 0 ]; then
281+
echo "## Failed Verifications" >> summary.md
282+
grep -l "❌ FAILED" verification_report_*.md | while read report; do
283+
echo "- $(basename $report)" >> summary.md
284+
done
285+
fi
286+
287+
cat summary.md
288+
289+
- name: Upload Summary
290+
uses: actions/upload-artifact@v4
291+
with:
292+
name: verification-summary
293+
path: summary.md

0 commit comments

Comments
 (0)