diff --git a/.devcontainer.json b/.devcontainer.json new file mode 100644 index 0000000..c6cb5a6 --- /dev/null +++ b/.devcontainer.json @@ -0,0 +1,3 @@ +{ + "image": "ghcr.io/bootc-dev/devenv-debian:latest" +} diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index b08f714..5c8e2a2 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -1,34 +1,42 @@ -name: Rust +name: CI + on: push: branches: [main] pull_request: branches: [main] + permissions: contents: read -# don't waste job slots on superseded code +# Don't waste job slots on superseded code concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true -env: - CARGO_TERM_COLOR: always - jobs: - tests-stable: - name: Tests, stable toolchain + ci: + name: CI + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Build and run CI in devcontainer + uses: devcontainers/ci@v0.3 + with: + push: never + runCmd: just ci + + kani: + name: Kani formal verification runs-on: ubuntu-latest steps: - - name: Check out repository + - name: Checkout uses: actions/checkout@v4 - - name: Install toolchain - uses: dtolnay/rust-toolchain@v1 + + - name: Run Kani proofs in devcontainer + uses: devcontainers/ci@v0.3 with: - toolchain: stable - - name: Cache build artifacts - uses: Swatinem/rust-cache@v2 - - name: cargo build - run: cargo build --all-targets - - name: cargo test - run: cargo test --all-targets + push: never + runCmd: just kani diff --git a/Cargo.toml b/Cargo.toml index 27b356e..8a7aab4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,6 +7,9 @@ authors = ["Colin Walters "] license = "MIT OR Apache-2.0" repository = "https://github.com/cgwalters/spec-json-rpc-fdpass" +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } + [dependencies] serde = { version = "1.0", features = ["derive"] } serde_json = "1.0" @@ -20,3 +23,4 @@ jsonrpsee = { version = "0.24", features = ["server", "client-core", "async-clie [dev-dependencies] tempfile = "3.0" async-trait = "0.1" +kani-verifier = "0.67" diff --git a/Justfile b/Justfile new file mode 100644 index 0000000..c41dee3 --- /dev/null +++ b/Justfile @@ -0,0 +1,58 @@ +# Format, lint, and type-check +check: + cargo fmt --check + cargo clippy --all-targets + cargo check --all-targets + +# Auto-format code +fmt: + cargo fmt + +# Run unit tests (uses nextest if available) +unit: + @if cargo nextest --version >/dev/null 2>&1; then \ + cargo nextest run; \ + else \ + cargo test; \ + fi + +# Run all tests +test-all: unit + +# Build release binaries +build: + cargo build --release + +# Build debug binaries +build-debug: + cargo build + +# Generate docs +doc: + cargo doc --no-deps + +# Open docs in browser +doc-open: + cargo doc --no-deps --open + +# Clean build artifacts +clean: + cargo clean + +# Full CI check (format, lint, test) +ci: check unit + +# Run Kani formal verification proofs +# NOTE: Kani requires rustup (won't work with distro-packaged Rust) +# Install: cargo install --locked kani-verifier && cargo kani setup +# Alternatively, Kani proofs run automatically in CI via GitHub Actions +kani: + cargo kani + +# Run a specific Kani proof by name +kani-proof name: + cargo kani --harness {{name}} + +# List available Kani proofs +kani-list: + cargo kani --list diff --git a/src/message.rs b/src/message.rs index 75d784b..79ca24e 100644 --- a/src/message.rs +++ b/src/message.rs @@ -20,7 +20,7 @@ pub fn get_fd_count(value: &serde_json::Value) -> usize { /// Helper to skip serializing fds field when it's None or 0 fn skip_if_zero_or_none(fds: &Option) -> bool { - fds.map_or(true, |n| n == 0) + fds.is_none_or(|n| n == 0) } /// A JSON-RPC 2.0 request message. @@ -256,3 +256,66 @@ pub fn file_descriptor_error() -> JsonRpcError<'static> { None::, ) } + +#[cfg(kani)] +mod verification { + use super::*; + + // ========================================================================= + // Proofs for skip_if_zero_or_none + // ========================================================================= + + /// Verify that skip_if_zero_or_none returns true for None + #[kani::proof] + fn check_skip_none() { + let result = skip_if_zero_or_none(&None); + kani::assert(result, "None should be skipped"); + } + + /// Verify that skip_if_zero_or_none returns true for Some(0) + #[kani::proof] + fn check_skip_zero() { + let result = skip_if_zero_or_none(&Some(0)); + kani::assert(result, "Some(0) should be skipped"); + } + + /// Verify that skip_if_zero_or_none returns false for any non-zero value + #[kani::proof] + fn check_skip_nonzero() { + let n: usize = kani::any(); + kani::assume(n > 0); + let result = skip_if_zero_or_none(&Some(n)); + kani::assert(!result, "Some(n > 0) should not be skipped"); + } + + // ========================================================================= + // Proofs for JsonRpcMessage::get_fds + // ========================================================================= + + /// Verify get_fds returns 0 when fds field is None + #[kani::proof] + fn check_get_fds_none() { + let msg = JsonRpcMessage::Notification(JsonRpcNotification { + jsonrpc: String::new(), + method: String::new(), + params: None, + fds: None, + }); + let result = msg.get_fds(); + kani::assert(result == 0, "None fds should return 0"); + } + + /// Verify get_fds returns the value when fds field is Some(n) + #[kani::proof] + fn check_get_fds_some() { + let n: usize = kani::any(); + let msg = JsonRpcMessage::Notification(JsonRpcNotification { + jsonrpc: String::new(), + method: String::new(), + params: None, + fds: Some(n), + }); + let result = msg.get_fds(); + kani::assert(result == n, "get_fds should return the fds value"); + } +} diff --git a/src/transport.rs b/src/transport.rs index 66ed8c3..26dcb6c 100644 --- a/src/transport.rs +++ b/src/transport.rs @@ -1,11 +1,11 @@ use crate::error::{Error, Result}; use crate::message::{get_fd_count, JsonRpcMessage, JsonRpcNotification, MessageWithFds}; use rustix::fd::AsFd; -use serde::Serialize; use rustix::net::{ RecvAncillaryBuffer, RecvAncillaryMessage, RecvFlags, SendAncillaryBuffer, SendAncillaryMessage, SendFlags, }; +use serde::Serialize; use std::collections::VecDeque; use std::io::{self, IoSlice, IoSliceMut}; use std::num::NonZeroUsize; @@ -148,7 +148,9 @@ impl Sender { let remaining_fds = &fds[fds_sent..]; // Determine how many FDs to send in this batch (up to current_max_fds) - let fds_batch = remaining_fds.get(..current_max_fds).unwrap_or(remaining_fds); + let fds_batch = remaining_fds + .get(..current_max_fds) + .unwrap_or(remaining_fds); let result = self .stream diff --git a/tests/integration_tests.rs b/tests/integration_tests.rs index cf13fa1..4a82763 100644 --- a/tests/integration_tests.rs +++ b/tests/integration_tests.rs @@ -195,9 +195,9 @@ async fn test_multiple_messages_with_fds_sequential() -> Result<()> { // Create multiple test files with different content let mut temp_files = Vec::new(); - let test_contents = vec!["Content 1", "Content 2", "Content 3"]; + let test_contents = ["Content 1", "Content 2", "Content 3"]; - for (_i, content) in test_contents.iter().enumerate() { + for content in test_contents.iter() { let mut temp_file = NamedTempFile::new().unwrap(); write!(temp_file, "{}", content).unwrap(); temp_file.flush().unwrap(); @@ -1932,7 +1932,10 @@ async fn test_fd_batching_one_per_message() -> Result<()> { assert_eq!(contents.trim(), expected, "FD {} has wrong content", i); } - Ok((Some(Value::String("All FDs verified".to_string())), Vec::new())) + Ok(( + Some(Value::String("All FDs verified".to_string())), + Vec::new(), + )) }); if let Ok((stream, _)) = listener.accept().await { @@ -2105,13 +2108,18 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> { tf.flush().unwrap(); temp_files.push(tf); } - let fds: Vec = temp_files.into_iter().map(|tf| tf.into_file().into()).collect(); + let fds: Vec = temp_files + .into_iter() + .map(|tf| tf.into_file().into()) + .collect(); let request = JsonRpcRequest::new( "with_fds".to_string(), Some(serde_json::json!({ "expected_fds": 3 })), Value::Number(1.into()), ); - sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), fds)).await?; + sender + .send(MessageWithFds::new(JsonRpcMessage::Request(request), fds)) + .await?; } // Message 2: No FDs @@ -2121,7 +2129,12 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> { Some(serde_json::json!({ "check": "first" })), Value::Number(2.into()), ); - sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), vec![])).await?; + sender + .send(MessageWithFds::new( + JsonRpcMessage::Request(request), + vec![], + )) + .await?; } // Message 3: 2 FDs @@ -2133,13 +2146,18 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> { tf.flush().unwrap(); temp_files.push(tf); } - let fds: Vec = temp_files.into_iter().map(|tf| tf.into_file().into()).collect(); + let fds: Vec = temp_files + .into_iter() + .map(|tf| tf.into_file().into()) + .collect(); let request = JsonRpcRequest::new( "with_fds".to_string(), Some(serde_json::json!({ "expected_fds": 2 })), Value::Number(3.into()), ); - sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), fds)).await?; + sender + .send(MessageWithFds::new(JsonRpcMessage::Request(request), fds)) + .await?; } // Message 4: No FDs @@ -2149,7 +2167,12 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> { Some(serde_json::json!({ "check": "second" })), Value::Number(4.into()), ); - sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), vec![])).await?; + sender + .send(MessageWithFds::new( + JsonRpcMessage::Request(request), + vec![], + )) + .await?; } // Message 5: 4 FDs @@ -2161,13 +2184,18 @@ async fn test_fd_batching_interleaved_with_no_fd_messages() -> Result<()> { tf.flush().unwrap(); temp_files.push(tf); } - let fds: Vec = temp_files.into_iter().map(|tf| tf.into_file().into()).collect(); + let fds: Vec = temp_files + .into_iter() + .map(|tf| tf.into_file().into()) + .collect(); let request = JsonRpcRequest::new( "with_fds".to_string(), Some(serde_json::json!({ "expected_fds": 4 })), Value::Number(5.into()), ); - sender.send(MessageWithFds::new(JsonRpcMessage::Request(request), fds)).await?; + sender + .send(MessageWithFds::new(JsonRpcMessage::Request(request), fds)) + .await?; } server_handle.abort();