diff --git a/.github/workflows/verify.yaml b/.github/workflows/verify.yaml new file mode 100644 index 000000000..0a954285b --- /dev/null +++ b/.github/workflows/verify.yaml @@ -0,0 +1,26 @@ +name: Verification +on: + pull_request: + merge_group: + +jobs: + verify-wire: + runs-on: [macos-latest] + steps: + - name: 'Checkout your code.' + uses: actions/checkout@v3 + + - name: 'Run Kani on TCP wire.' + uses: model-checking/kani-github-action@v0.33 + with: + args: '--output-format=terse --verbose --harness wire::tcp::verification' + verify-socket: + runs-on: [macos-latest] + steps: + - name: 'Checkout your code.' + uses: actions/checkout@v3 + + - name: 'Run Kani on TCP socket.' + uses: model-checking/kani-github-action@v0.33 + with: + args: '--output-format=terse --verbose --harness socket::tcp::verification' diff --git a/src/iface/interface/mod.rs b/src/iface/interface/mod.rs index bd682496d..f32fc7899 100644 --- a/src/iface/interface/mod.rs +++ b/src/iface/interface/mod.rs @@ -968,7 +968,7 @@ impl InterfaceInner { None } - #[cfg(test)] + #[cfg(any(test, kani))] #[allow(unused)] // unused depending on which sockets are enabled pub(crate) fn set_now(&mut self, now: Instant) { self.now = now diff --git a/src/lib.rs b/src/lib.rs index 5f38606a8..8a5c5e5e5 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -129,7 +129,7 @@ mod macros; mod parsers; mod rand; -#[cfg(test)] +#[cfg(any(test, kani))] mod config { #![allow(unused)] pub const ASSEMBLER_MAX_SEGMENT_COUNT: usize = 4; @@ -149,7 +149,7 @@ mod config { pub const IPV6_HBH_MAX_OPTIONS: usize = 2; } -#[cfg(not(test))] +#[cfg(not(any(test, kani)))] mod config { #![allow(unused)] include!(concat!(env!("OUT_DIR"), "/config.rs")); @@ -170,7 +170,7 @@ pub mod time; pub mod wire; #[cfg(all( - test, + any(test, kani), any( feature = "medium-ethernet", feature = "medium-ip", diff --git a/src/socket/tcp.rs b/src/socket/tcp.rs index 79caf8c83..7e689809d 100644 --- a/src/socket/tcp.rs +++ b/src/socket/tcp.rs @@ -107,6 +107,7 @@ pub type SocketBuffer<'a> = RingBuffer<'a, u8>; /// [RFC 793]: https://tools.ietf.org/html/rfc793 #[derive(Debug, PartialEq, Eq, Clone, Copy)] #[cfg_attr(feature = "defmt", derive(defmt::Format))] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub enum State { Closed, Listen, @@ -152,6 +153,7 @@ const RTTE_MAX_RTO: u32 = 10000; #[derive(Debug, Clone, Copy)] #[cfg_attr(feature = "defmt", derive(defmt::Format))] +#[cfg_attr(kani, derive(kani::Arbitrary, PartialEq))] struct RttEstimator { // Using u32 instead of Duration to save space (Duration is i64) rtt: u32, @@ -249,6 +251,7 @@ impl RttEstimator { #[derive(Debug, Clone, Copy, PartialEq)] #[cfg_attr(feature = "defmt", derive(defmt::Format))] +#[cfg_attr(kani, derive(kani::Arbitrary))] enum Timer { Idle { keep_alive_at: Option, @@ -371,6 +374,7 @@ impl Timer { } #[derive(Debug, PartialEq, Eq, Clone, Copy)] +#[cfg_attr(kani, derive(kani::Arbitrary))] enum AckDelayTimer { Idle, Waiting(Instant), @@ -379,6 +383,7 @@ enum AckDelayTimer { #[derive(Debug, Copy, Clone, Eq, PartialEq)] #[cfg_attr(feature = "defmt", derive(defmt::Format))] +#[cfg_attr(kani, derive(kani::Arbitrary))] struct Tuple { local: IpEndpoint, remote: IpEndpoint, @@ -489,9 +494,8 @@ impl<'a> Socket<'a> { if rx_capacity > (1 << 30) { panic!("receiving buffer too large, cannot exceed 1 GiB") } - let rx_cap_log2 = mem::size_of::() * 8 - rx_capacity.leading_zeros() as usize; - Socket { + let mut socket = Socket { state: State::Closed, timer: Timer::new(), rtte: RttEstimator::default(), @@ -510,7 +514,7 @@ impl<'a> Socket<'a> { remote_last_ack: None, remote_last_win: 0, remote_win_len: 0, - remote_win_shift: rx_cap_log2.saturating_sub(16) as u8, + remote_win_shift: 0, remote_win_scale: None, remote_has_sack: false, remote_mss: DEFAULT_MSS, @@ -527,7 +531,17 @@ impl<'a> Socket<'a> { rx_waker: WakerRegistration::new(), #[cfg(feature = "async")] tx_waker: WakerRegistration::new(), - } + }; + + socket.compute_win_shift(); + + socket + } + + pub fn compute_win_shift(&mut self) { + let rx_cap_log2 = + mem::size_of::() * 8 - self.rx_buffer.capacity().leading_zeros() as usize; + self.remote_win_shift = rx_cap_log2.saturating_sub(16) as u8; } /// Register a waker for receive operations. @@ -710,9 +724,6 @@ impl<'a> Socket<'a> { } fn reset(&mut self) { - let rx_cap_log2 = - mem::size_of::() * 8 - self.rx_buffer.capacity().leading_zeros() as usize; - self.state = State::Closed; self.timer = Timer::new(); self.rtte = RttEstimator::default(); @@ -729,12 +740,13 @@ impl<'a> Socket<'a> { self.remote_last_win = 0; self.remote_win_len = 0; self.remote_win_scale = None; - self.remote_win_shift = rx_cap_log2.saturating_sub(16) as u8; self.remote_mss = DEFAULT_MSS; self.remote_last_ts = None; self.ack_delay_timer = AckDelayTimer::Idle; self.challenge_ack_timer = Instant::from_secs(0); + self.compute_win_shift(); + #[cfg(feature = "async")] { self.rx_waker.wake(); @@ -2390,6 +2402,52 @@ impl<'a> fmt::Write for Socket<'a> { } } +#[cfg(kani)] +impl<'a> kani::Arbitrary for Socket<'a> { + #[inline] + fn any() -> Self { + // These bounds are enforced by Socket::new(). + let rx_buffer_size: usize = kani::any_where(|s| *s <= (1 << 30)); + let tx_buffer_size: usize = kani::any_where(|s| *s <= (1 << 30)); + return Socket { + state: kani::any(), + timer: kani::any(), + rtte: kani::any(), + assembler: Assembler::new(), + rx_buffer: SocketBuffer::new(vec![0; rx_buffer_size]), + rx_fin_received: kani::any(), + tx_buffer: SocketBuffer::new(vec![0; tx_buffer_size]), + timeout: kani::any(), + keep_alive: kani::any(), + hop_limit: kani::any(), + listen_endpoint: kani::any(), + tuple: kani::any(), + local_seq_no: kani::any(), + remote_seq_no: kani::any(), + remote_last_seq: kani::any(), + remote_last_ack: kani::any(), + remote_last_win: kani::any(), + remote_win_shift: kani::any(), + remote_win_len: kani::any(), + remote_win_scale: kani::any(), + remote_has_sack: kani::any(), + remote_mss: kani::any(), + remote_last_ts: kani::any(), + local_rx_last_seq: kani::any(), + local_rx_last_ack: kani::any(), + local_rx_dup_acks: kani::any(), + ack_delay: kani::any(), + ack_delay_timer: kani::any(), + challenge_ack_timer: kani::any(), + nagle: kani::any(), + #[cfg(feature = "async")] + rx_waker: WakerRegistration::new(), + #[cfg(feature = "async")] + tx_waker: WakerRegistration::new(), + }; + } +} + // TODO: TCP should work for all features. For now, we only test with the IP feature. We could do // it for other features as well with rstest, however, this means we have to modify a lot of the // tests in here, which I didn't had the time for at the moment. @@ -7259,3 +7317,642 @@ mod test { } } } + +#[cfg(kani)] +mod verification { + extern crate kani; + use super::*; + use crate::wire::IpRepr; + use std::ops::{Deref, DerefMut}; + + // =========================================================================================// + // Helper functions + // =========================================================================================// + + struct TestSocket { + socket: Socket<'static>, + cx: Context, + tuple: Tuple, + } + + impl Deref for TestSocket { + type Target = Socket<'static>; + fn deref(&self) -> &Self::Target { + &self.socket + } + } + + impl DerefMut for TestSocket { + fn deref_mut(&mut self) -> &mut Self::Target { + &mut self.socket + } + } + + impl kani::Arbitrary for TestSocket { + #[inline] + fn any() -> Self { + let mut socket: Socket = kani::any(); + socket.set_ack_delay(None); + let (iface, _, _) = crate::tests::setup(crate::phy::Medium::Ip); + let ipv4: bool = kani::any(); + let tuple: Tuple = Tuple { + local: IpEndpoint { + addr: kani::any_where(|a| ipv4 == matches!(a, IpAddress::Ipv4(_))), + port: kani::any_where(|p| *p != 0), + }, + remote: IpEndpoint { + addr: kani::any_where(|a| ipv4 == matches!(a, IpAddress::Ipv4(_))), + port: kani::any_where(|p| *p != 0), + }, + }; + return TestSocket { + socket, + cx: iface.inner, + tuple, + }; + } + } + + fn send( + socket: &mut TestSocket, + timestamp: Instant, + repr: &TcpRepr, + ) -> Option> { + socket.cx.set_now(timestamp); + + let ip_repr: IpRepr = IpRepr::new( + socket.tuple.remote.addr, + socket.tuple.local.addr, + IpProtocol::Tcp, + repr.buffer_len(), + kani::any(), + ); + net_trace!("send: {}", repr); + + assert!(socket.socket.accepts(&mut socket.cx, &ip_repr, repr)); + + match socket.socket.process(&mut socket.cx, &ip_repr, repr) { + Some((_ip_repr, repr)) => { + net_trace!("recv: {}", repr); + Some(repr) + } + None => None, + } + } + + fn recv(socket: &mut TestSocket, timestamp: Instant, mut f: F) + where + F: FnMut(Result), + { + socket.cx.set_now(timestamp); + + let local_addr = socket.tuple.local.addr; + let remote_addr = socket.tuple.remote.addr; + + let mut sent = 0; + let result = socket + .socket + .dispatch(&mut socket.cx, |_, (ip_repr, tcp_repr)| { + assert_eq!(ip_repr.next_header(), IpProtocol::Tcp); + assert_eq!(ip_repr.src_addr(), local_addr); + assert_eq!(ip_repr.dst_addr(), remote_addr); + assert_eq!(ip_repr.payload_len(), tcp_repr.buffer_len()); + + net_trace!("recv: {}", tcp_repr); + sent += 1; + Ok(f(Ok(tcp_repr))) + }); + match result { + Ok(()) => assert_eq!(sent, 1, "Exactly one packet should be sent"), + Err(e) => f(Err(e)), + } + } + + macro_rules! send { + ($socket:ident, $repr:expr) => + (send!($socket, time 0, $repr)); + ($socket:ident, $repr:expr, $result:expr) => + (send!($socket, time 0, $repr, $result)); + ($socket:ident, time $time:expr, $repr:expr) => + (send!($socket, time $time, $repr, None)); + ($socket:ident, time $time:expr, $repr:expr, $result:expr) => + (assert_eq!(send(&mut $socket, Instant::from_millis($time), &$repr), $result)); + } + + // =========================================================================================// + // Proofs + // =========================================================================================// + + #[kani::proof] + fn prove_closed_reject() { + let mut socket: TestSocket = kani::any_where(|s: &TestSocket| s.state == State::Closed); + assert_eq!(socket.state, State::Closed); + + let tcp_repr: TcpRepr = kani::any(); + let send_ip: IpRepr = kani::any(); + + assert!(!socket.socket.accepts(&mut socket.cx, &send_ip, &tcp_repr)); + } + + #[kani::proof] + fn prove_closed_reject_after_listen() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| s.state == State::Closed); + let local_endpoint: IpEndpoint = kani::any(); + s.listen(local_endpoint).unwrap(); + s.close(); + + let tcp_repr: TcpRepr = kani::any(); + let send_ip: IpRepr = kani::any(); + + assert!(!s.socket.accepts(&mut s.cx, &send_ip, &tcp_repr)); + } + + #[kani::proof] + fn prove_closed_close() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + matches!(s.state, State::Closed | State::Listen | State::SynSent) + }); + s.close(); + assert_eq!(s.state, State::Closed); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_listen_sack_option() { + let sack_enabled: bool = kani::any(); + + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + s.timer == Timer::new() + && s.rtte == RttEstimator::default() + && s.timeout == None + && s.rx_buffer.capacity() > 3 + && s.tx_buffer.capacity() > 3 + && s.state == State::Listen + && s.socket.tuple.is_none() + && s.listen_endpoint.addr.is_none() + && s.listen_endpoint.port == s.tuple.local.port + }); + s.compute_win_shift(); + + let packet_to_send: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::Syn + && p.max_seg_size != Some(0) + && p.ack_number.is_none() + && p.sack_ranges == [None, None, None] + && p.sack_permitted == sack_enabled + }); + + send!(s, packet_to_send); + assert_eq!(s.state, State::SynReceived); + assert_eq!(s.remote_has_sack, sack_enabled); + + recv(&mut s, Instant::from_secs(0), |repr| { + assert!(repr.is_ok()); + assert_eq!(repr.unwrap().control, TcpControl::Syn); + assert_eq!( + repr.unwrap().ack_number, + Some(packet_to_send.seq_number + 1) + ); + assert_eq!(repr.unwrap().sack_permitted, sack_enabled); + }); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_listen_syn_win_scale_buffers() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| + // Needed to prevent socket timeout. + s.timer == Timer::new() && + s.timeout == None && + s.remote_last_ts == None && + s.rtte == RttEstimator::default() && + + s.state == State::Listen && + s.socket.tuple.is_none() && + s.listen_endpoint.addr.is_none() && + s.listen_endpoint.port == s.tuple.local.port); + s.compute_win_shift(); + + let window_shift = s.remote_win_shift; + + let packet_to_send: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::Syn + && p.max_seg_size != Some(0) + && p.ack_number.is_none() + && p.window_scale == Some(0) + }); + + send!(s, packet_to_send); + let buffer_capacity = s.rx_buffer.window(); + + recv(&mut s, Instant::from_secs(0), |repr| { + assert!(repr.is_ok()); + assert!(repr.unwrap().control == TcpControl::Syn); + assert_eq!( + repr.unwrap().ack_number, + Some(packet_to_send.seq_number + 1) + ); + assert_eq!(repr.unwrap().window_scale, Some(window_shift)); + assert_eq!( + repr.unwrap().window_len, + cmp::min(buffer_capacity, 65535) as u16 + ); + }); + } + + #[kani::proof] + fn prove_listen_validation() { + let mut s: TestSocket = kani::any(); + assert_eq!(s.listen(0), Err(ListenError::Unaddressable)); + } + + #[kani::proof] + fn prove_listen_twice() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| !s.is_open()); + let port1: u16 = kani::any_where(|p| *p != 0); + let port2: u16 = kani::any_where(|p| *p != 0 && *p != port1); + assert_eq!(s.listen(port1), Ok(())); + assert!(s.is_open()); + assert_eq!(s.listen(port2), Err(ListenError::InvalidState)); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_listen_syn() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + s.state == State::Listen + && s.socket.tuple.is_none() + && s.listen_endpoint.addr.is_none() + && s.listen_endpoint.port == s.tuple.local.port + }); + + let packet_to_send: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::Syn + && p.max_seg_size != Some(0) + && p.ack_number.is_none() + }); + + send!(s, packet_to_send); + + assert_eq!(s.state, State::SynReceived); + assert_eq!(s.socket.tuple, Some(s.tuple)); + assert_eq!(s.remote_seq_no, packet_to_send.seq_number + 1); + assert_eq!(s.remote_has_sack, packet_to_send.sack_permitted); + assert_eq!(s.remote_win_scale, packet_to_send.window_scale); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_listen_syn_reject_ack() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + s.state == State::Listen + && s.socket.tuple.is_none() + && s.listen_endpoint.addr.is_none() + && s.listen_endpoint.port == s.tuple.local.port + }); + + let send_ip: IpRepr = kani::any(); + let packet_to_send: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::Syn + && p.ack_number.is_some() + }); + + assert!(!s.socket.accepts(&mut s.cx, &send_ip, &packet_to_send)); + assert_eq!(s.state, State::Listen); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_listen_rst() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + s.state == State::Listen + && s.socket.tuple.is_none() + && s.listen_endpoint.addr.is_none() + && s.listen_endpoint.port == s.tuple.local.port + }); + + let packet_to_send: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::Rst + && p.ack_number.is_none() + }); + + send!(s, packet_to_send); + assert_eq!(s.state, State::Listen); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_listen_close() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| s.state == State::Listen); + + s.close(); + + assert_eq!(s.state, State::Closed); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_syn_received_ack() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + // Needed to prevent socket timeout. + s.timer == Timer::new() + && s.rx_buffer.capacity() != 0 + && s.tx_buffer.capacity() != 0 + && s.timeout == None + && s.remote_win_scale == None + && s.rtte == RttEstimator::default() + && s.local_seq_no == s.remote_last_seq + && s.state == State::SynReceived + && s.socket.tuple == Some(s.tuple) + && s.listen_endpoint.addr.is_none() + && s.listen_endpoint.port == s.tuple.local.port + }); + s.compute_win_shift(); + + let local_seq = s.local_seq_no; + let remote_seq = s.remote_seq_no - 1; + let local_port = s.tuple.local.port; + let remote_port = s.tuple.remote.port; + + recv(&mut s, Instant::from_secs(0), |repr| { + assert!(repr.is_ok()); + assert_eq!(repr.unwrap().control, TcpControl::Syn); + assert_eq!(repr.unwrap().src_port, local_port); + assert_eq!(repr.unwrap().dst_port, remote_port); + assert_eq!(repr.unwrap().seq_number, local_seq); + assert_eq!(repr.unwrap().ack_number, Some(remote_seq + 1)); + }); + + let packet_to_send: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::None + && p.ack_number == Some(local_seq + 1) + && p.seq_number == remote_seq + 1 + }); + + send!(s, packet_to_send); + assert_eq!(s.state, State::Established); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_syn_received_ack_invalid() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + // Needed to prevent socket timeout. + s.timer == Timer::new() + && s.rx_buffer.capacity() != 0 + && s.tx_buffer.capacity() != 0 + && s.timeout == None + && s.remote_win_scale == None + && s.rtte == RttEstimator::default() + && s.local_seq_no == s.remote_last_seq + && s.state == State::SynReceived + && s.socket.tuple == Some(s.tuple) + && s.listen_endpoint.addr.is_none() + && s.listen_endpoint.port == s.tuple.local.port + }); + s.compute_win_shift(); + + let local_seq = s.local_seq_no; + let remote_seq = s.remote_seq_no - 1; + let local_port = s.tuple.local.port; + let remote_port = s.tuple.remote.port; + + recv(&mut s, Instant::from_secs(0), |repr| { + assert!(repr.is_ok()); + assert_eq!(repr.unwrap().control, TcpControl::Syn); + assert_eq!(repr.unwrap().src_port, local_port); + assert_eq!(repr.unwrap().dst_port, remote_port); + assert_eq!(repr.unwrap().seq_number, local_seq); + assert_eq!(repr.unwrap().ack_number, Some(remote_seq + 1)); + }); + + let wrong_ack: TcpSeqNumber = kani::any_where(|s: &TcpSeqNumber| *s != local_seq + 1); + + let packet_in: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port && + p.dst_port == s.tuple.local.port && + p.control == TcpControl::None && + p.ack_number == Some(wrong_ack) && // wrong + p.seq_number == remote_seq + 1 + }); + + let packet_out = send(&mut s, Instant::from_millis(0), &packet_in); + assert!(packet_out.is_some()); + assert_eq!(packet_out.unwrap().src_port, local_port); + assert_eq!(packet_out.unwrap().dst_port, remote_port); + assert_eq!(packet_out.unwrap().control, TcpControl::Rst); + assert_eq!(packet_out.unwrap().ack_number, None); + assert_eq!(packet_out.unwrap().seq_number, wrong_ack); + assert_eq!(packet_out.unwrap().window_len, 0); + + assert_eq!(s.state, State::SynReceived); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_syn_received_fin() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + // Needed to prevent socket timeout. + s.timer == Timer::new() + && s.rx_buffer.capacity() > 3 + && s.tx_buffer.capacity() > 3 + && s.timeout == None + && s.remote_win_scale == None + && s.rtte == RttEstimator::default() + && s.local_seq_no == s.remote_last_seq + && s.state == State::SynReceived + && s.socket.tuple == Some(s.tuple) + && s.listen_endpoint.addr.is_none() + && s.listen_endpoint.port == s.tuple.local.port + }); + s.compute_win_shift(); + + let local_seq = s.local_seq_no; + let remote_seq = s.remote_seq_no - 1; + let local_port = s.tuple.local.port; + let remote_port = s.tuple.remote.port; + + recv(&mut s, Instant::from_secs(0), |repr| { + assert!(repr.is_ok()); + assert_eq!(repr.unwrap().control, TcpControl::Syn); + assert_eq!(repr.unwrap().src_port, local_port); + assert_eq!(repr.unwrap().dst_port, remote_port); + assert_eq!(repr.unwrap().seq_number, local_seq); + assert_eq!(repr.unwrap().ack_number, Some(remote_seq + 1)); + }); + + let packet_in: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::Fin + && p.ack_number == Some(local_seq + 1) + && p.seq_number == remote_seq + 1 + && p.max_seg_size == None + && p.window_scale == None + && p.window_len == 256 + }); + + send!(s, packet_in); + + recv(&mut s, Instant::from_secs(0), |repr| { + assert!(repr.is_ok()); + assert_eq!(repr.unwrap().control, TcpControl::None); + assert_eq!(repr.unwrap().src_port, local_port); + assert_eq!(repr.unwrap().dst_port, remote_port); + // Check for keep-alive. + assert!( + repr.unwrap().seq_number == local_seq + 1 + || (repr.unwrap().seq_number == local_seq && repr.unwrap().payload == b"\x00") + ); + assert_eq!( + repr.unwrap().ack_number, + Some(remote_seq + 1 + packet_in.payload.len() + 1) + ); + }); + + assert_eq!(s.state, State::CloseWait); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_syn_received_rst() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + // Needed to prevent socket timeout. + s.timer == Timer::new() + && s.rx_buffer.capacity() > 3 + && s.tx_buffer.capacity() > 3 + && s.timeout == None + && s.remote_win_scale == None + && s.rtte == RttEstimator::default() + && s.local_seq_no == s.remote_last_seq + && s.state == State::SynReceived + && s.socket.tuple == Some(s.tuple) + && s.listen_endpoint.addr.is_none() + && s.listen_endpoint.port == s.tuple.local.port + }); + s.compute_win_shift(); + + let local_seq = s.local_seq_no; + let remote_seq = s.remote_seq_no - 1; + let local_port = s.tuple.local.port; + let remote_port = s.tuple.remote.port; + + recv(&mut s, Instant::from_secs(0), |repr| { + assert!(repr.is_ok()); + assert_eq!(repr.unwrap().control, TcpControl::Syn); + assert_eq!(repr.unwrap().src_port, local_port); + assert_eq!(repr.unwrap().dst_port, remote_port); + assert_eq!(repr.unwrap().seq_number, local_seq); + assert_eq!(repr.unwrap().ack_number, Some(remote_seq + 1)); + }); + + let packet_in: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::Rst + && p.ack_number == Some(local_seq) + && p.seq_number == remote_seq + 1 + }); + + send!(s, packet_in); + + assert_eq!(s.state, State::Listen); + assert_eq!(s.listen_endpoint.addr, None); + assert_eq!(s.listen_endpoint.port, s.tuple.local.port); + assert_eq!(s.socket.tuple, None); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_syn_received_window_scaling() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| { + s.state == State::Listen + && s.timer == Timer::new() + && s.rtte == RttEstimator::default() + && s.timeout == None + && s.rx_buffer.capacity() > 3 + && s.tx_buffer.capacity() > 3 + && s.socket.tuple.is_none() + && s.listen_endpoint.addr.is_none() + && s.listen_endpoint.port == s.tuple.local.port + && s.local_seq_no == s.remote_last_seq + }); + s.compute_win_shift(); + + let remote_seq = s.remote_seq_no - 1; + let local_port = s.tuple.local.port; + let remote_port = s.tuple.remote.port; + + let window_scale: Option = kani::any_where(|w: &Option| { + w.is_none() || (w.is_some() && *w >= Some(0) && *w <= Some(14)) + }); + + let packet_in: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::Syn + && p.ack_number == None + && p.seq_number == remote_seq + && p.max_seg_size != Some(0) + && p.window_scale == window_scale + }); + + send!(s, packet_in); + + assert_eq!(s.state, State::SynReceived); + assert_eq!(s.socket.tuple, Some(s.tuple)); + + let local_seq = s.local_seq_no; + let recv_win_scale = if window_scale.is_none() { + None + } else { + Some(s.remote_win_shift) + }; + + recv(&mut s, Instant::from_secs(0), |repr| { + assert!(repr.is_ok()); + assert_eq!(repr.unwrap().control, TcpControl::Syn); + assert_eq!(repr.unwrap().src_port, local_port); + assert_eq!(repr.unwrap().dst_port, remote_port); + assert_eq!(repr.unwrap().seq_number, local_seq); + assert_eq!(repr.unwrap().ack_number, Some(remote_seq + 1)); + assert_eq!(repr.unwrap().window_scale, recv_win_scale); + }); + + let packet_in: TcpRepr = kani::any_where(|p: &TcpRepr| { + p.src_port == s.tuple.remote.port + && p.dst_port == s.tuple.local.port + && p.control == TcpControl::None + && p.ack_number == Some(local_seq + 1) + && p.seq_number == remote_seq + 1 + && p.max_seg_size != Some(0) + && p.window_scale == None + }); + + send!(s, packet_in); + + assert_eq!(s.remote_win_scale, window_scale); + } + + #[kani::proof] + #[kani::unwind(20)] + fn prove_syn_received_close() { + let mut s: TestSocket = kani::any_where(|s: &TestSocket| s.state == State::SynReceived); + + s.close(); + + assert_eq!(s.state, State::FinWait1); + } +} diff --git a/src/time.rs b/src/time.rs index 318dacacb..f8bea4d5b 100644 --- a/src/time.rs +++ b/src/time.rs @@ -22,6 +22,7 @@ use core::{fmt, ops}; /// * A value less than `0` indicates a time before the starting /// point. #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Instant { micros: i64, } @@ -178,6 +179,7 @@ impl ops::Sub for Instant { /// A relative amount of time. #[derive(Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Duration { micros: u64, } diff --git a/src/wire/ip.rs b/src/wire/ip.rs index da80aba3f..1a153897d 100644 --- a/src/wire/ip.rs +++ b/src/wire/ip.rs @@ -47,6 +47,7 @@ impl fmt::Display for Version { enum_with_unknown! { /// IP datagram encapsulated protocol. + #[cfg_attr(kani, derive(kani::Arbitrary))] pub enum Protocol(u8) { HopByHop = 0x00, Icmp = 0x01, @@ -85,6 +86,7 @@ impl fmt::Display for Protocol { /// An internetworking address. #[derive(Debug, Hash, PartialEq, Eq, PartialOrd, Ord, Clone, Copy)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub enum Address { /// An IPv4 address. #[cfg(feature = "proto-ipv4")] @@ -447,6 +449,16 @@ impl> From<(T, u16)> for Endpoint { } } +#[cfg(kani)] +impl<'a> kani::Arbitrary for Endpoint { + #[inline] + fn any() -> Self { + let addr: Address = kani::any(); + let port: u16 = kani::any_where(|p| *p != 0); + return Self::new(addr, port); + } +} + /// An internet endpoint address for listening. /// /// In contrast with [`Endpoint`], `ListenEndpoint` allows not specifying the address, @@ -454,6 +466,7 @@ impl> From<(T, u16)> for Endpoint { /// /// An endpoint can be constructed from a port, in which case the address is unspecified. #[derive(Debug, Hash, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct ListenEndpoint { pub addr: Option
, pub port: u16, @@ -543,6 +556,7 @@ impl> From<(T, u16)> for ListenEndpoint { /// or IPv6 concrete high-level representation. #[derive(Debug, Clone, PartialEq, Eq)] #[cfg_attr(feature = "defmt", derive(defmt::Format))] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub enum Repr { #[cfg(feature = "proto-ipv4")] Ipv4(Ipv4Repr), diff --git a/src/wire/ipv4.rs b/src/wire/ipv4.rs index 1027fc262..d3f1d9038 100644 --- a/src/wire/ipv4.rs +++ b/src/wire/ipv4.rs @@ -37,6 +37,7 @@ pub struct Key { /// A four-octet IPv4 address. #[derive(Debug, Hash, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Address(pub [u8; ADDR_SIZE]); impl Address { @@ -619,6 +620,7 @@ impl> AsRef<[u8]> for Packet { /// A high-level representation of an Internet Protocol version 4 packet header. #[derive(Debug, PartialEq, Eq, Clone, Copy)] #[cfg_attr(feature = "defmt", derive(defmt::Format))] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Repr { pub src_addr: Address, pub dst_addr: Address, diff --git a/src/wire/ipv6.rs b/src/wire/ipv6.rs index d624f246d..3ed47d5df 100644 --- a/src/wire/ipv6.rs +++ b/src/wire/ipv6.rs @@ -27,6 +27,7 @@ pub const IPV4_MAPPED_PREFIX_SIZE: usize = ADDR_SIZE - 4; // 4 == ipv4::ADDR_SIZ /// A sixteen-octet IPv6 address. #[derive(Debug, Hash, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Address(pub [u8; ADDR_SIZE]); impl Address { @@ -721,6 +722,7 @@ impl> AsRef<[u8]> for Packet { /// A high-level representation of an Internet Protocol version 6 packet header. #[derive(Debug, PartialEq, Eq, Clone, Copy)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct Repr { /// IPv6 address of the source node. pub src_addr: Address, diff --git a/src/wire/tcp.rs b/src/wire/tcp.rs index 24821430a..e654aaa87 100644 --- a/src/wire/tcp.rs +++ b/src/wire/tcp.rs @@ -11,6 +11,7 @@ use crate::wire::{IpAddress, IpProtocol}; /// A sequence number is a monotonically advancing integer modulo 232. /// Sequence numbers do not have a discontiguity when compared pairwise across a signed overflow. #[derive(Debug, PartialEq, Eq, Clone, Copy, Default)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct SeqNumber(pub i32); impl SeqNumber { @@ -614,6 +615,42 @@ impl> AsRef<[u8]> for Packet { } } +#[cfg(kani)] +impl kani::Arbitrary for Packet> { + #[inline] + fn any() -> Self { + // FIXME: Packets with symbolic payload length are too expensive (dozens of hours). + // FIXME: checksums are quite expensive (one hour). + let options: Vec = kani::vec::exact_vec::<_, 4>(); + let payload: Vec = kani::vec::exact_vec::<_, 8>(); + + let bytes: Vec = vec![0xa5; 32]; + let mut packet = Packet::new_unchecked(bytes); + + packet.set_src_port(kani::any()); + packet.set_dst_port(kani::any()); + packet.set_seq_number(kani::any()); + packet.set_ack_number(kani::any()); + packet.set_header_len(24); + packet.clear_flags(); + packet.set_fin(kani::any()); + packet.set_syn(kani::any()); + packet.set_rst(kani::any()); + packet.set_psh(kani::any()); + packet.set_ack(kani::any()); + packet.set_urg(kani::any()); + packet.set_ece(kani::any()); + packet.set_cwr(kani::any()); + packet.set_ns(kani::any()); + packet.set_window_len(kani::any()); + packet.set_urgent_at(kani::any()); + packet.options_mut().copy_from_slice(&options[..]); + packet.payload_mut().copy_from_slice(&payload[..]); + + return packet; + } +} + /// A representation of a single TCP option. #[derive(Debug, PartialEq, Eq, Clone, Copy)] #[cfg_attr(feature = "defmt", derive(defmt::Format))] @@ -763,9 +800,48 @@ impl<'a> TcpOption<'a> { } } +#[cfg(kani)] +impl<'a> kani::Arbitrary for TcpOption<'a> { + #[inline] + fn any() -> Self { + let option: u8 = kani::any_where(|v| *v >= 1 && *v <= 7); + return match option { + 1 => TcpOption::EndOfList, + 2 => TcpOption::NoOperation, + 3 => TcpOption::MaxSegmentSize(kani::any()), + 4 => TcpOption::WindowScale(kani::any()), + 5 => TcpOption::SackPermitted, + 6 => { + let range_type: u8 = kani::any_where(|v| *v >= 1 && *v <= 3); + let ranges: [Option<(u32, u32)>; 3] = match range_type { + 1 => [Some((kani::any(), kani::any())), None, None], + 2 => [ + Some((kani::any(), kani::any())), + Some((kani::any(), kani::any())), + None, + ], + 3 => [ + Some((kani::any(), kani::any())), + Some((kani::any(), kani::any())), + Some((kani::any(), kani::any())), + ], + _ => unreachable!(), + }; + return TcpOption::SackRange(ranges); + } + 7 => TcpOption::Unknown { + kind: kani::any_where(|v| *v > 5), + data: kani::vec::exact_vec::().leak(), + }, + _ => unreachable!(), + }; + } +} + /// The possible control flags of a Transmission Control Protocol packet. #[derive(Debug, PartialEq, Eq, Clone, Copy)] #[cfg_attr(feature = "defmt", derive(defmt::Format))] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub enum Control { None, Psh, @@ -1008,6 +1084,45 @@ impl<'a> Repr<'a> { } } +#[cfg(kani)] +impl<'a> kani::Arbitrary for Repr<'a> { + #[inline] + fn any() -> Self { + // Limit payload to length 4 to keep things reasonable. + let payload: Vec = kani::vec::exact_vec::(); + let range_type: u8 = kani::any_where(|v| *v >= 1 && *v <= 4); + let ranges: [Option<(u32, u32)>; 3] = match range_type { + 1 => [None, None, None], + 2 => [Some((kani::any(), kani::any())), None, None], + 3 => [ + Some((kani::any(), kani::any())), + Some((kani::any(), kani::any())), + None, + ], + 4 => [ + Some((kani::any(), kani::any())), + Some((kani::any(), kani::any())), + Some((kani::any(), kani::any())), + ], + _ => unreachable!(), + }; + return Repr { + src_port: kani::any_where(|p| *p != 0), + dst_port: kani::any_where(|p| *p != 0), + seq_number: kani::any(), + ack_number: kani::any(), + window_len: kani::any(), + // This is enforced by parse(). + window_scale: kani::any_where(|s: &Option| s.is_none() || s.unwrap() <= 14), + control: kani::any(), + max_seg_size: kani::any(), + sack_permitted: kani::any(), + sack_ranges: ranges, + payload: payload.leak(), + }; + } +} + impl<'a, T: AsRef<[u8]> + ?Sized> fmt::Display for Packet<&'a T> { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { // Cannot use Repr::parse because we don't have the IP addresses. @@ -1329,3 +1444,156 @@ mod test { assert_eq!(TcpOption::parse(&[0x3, 0x02]), Err(Error)); } } + +#[cfg(kani)] +mod verification { + + extern crate kani; + use super::*; + use alloc::vec; + + use crate::wire::Ipv4Address; + + #[kani::proof] + #[kani::unwind(10)] + fn prove_parsing() { + let src_port: u16 = kani::any(); + let dst_port: u16 = kani::any(); + + let seq_number: SeqNumber = kani::any(); + let ack_number: SeqNumber = kani::any(); + + let fin: bool = kani::any(); + let syn: bool = kani::any(); + let rst: bool = kani::any(); + let psh: bool = kani::any(); + let ack: bool = kani::any(); + let urg: bool = kani::any(); + let ece: bool = kani::any(); + let cwr: bool = kani::any(); + let ns: bool = kani::any(); + + let window_len: u16 = kani::any(); + let urgent_at: u16 = kani::any(); + + let options: Vec = kani::vec::exact_vec::<_, 4>(); + let payload: Vec = kani::vec::exact_vec::<_, 8>(); + + let mut bytes = vec![0xa5; 32]; + let mut packet = Packet::new_unchecked(&mut bytes); + packet.set_src_port(src_port); + packet.set_dst_port(dst_port); + packet.set_seq_number(seq_number); + packet.set_ack_number(ack_number); + packet.set_header_len(24); + packet.clear_flags(); + packet.set_fin(fin); + packet.set_syn(syn); + packet.set_rst(rst); + packet.set_psh(psh); + packet.set_ack(ack); + packet.set_urg(urg); + packet.set_ece(ece); + packet.set_cwr(cwr); + packet.set_ns(ns); + packet.set_window_len(window_len); + packet.set_urgent_at(urgent_at); + packet.options_mut().copy_from_slice(&options[..]); + packet.payload_mut().copy_from_slice(&payload[..]); + + assert_eq!(src_port, packet.src_port()); + assert_eq!(dst_port, packet.dst_port()); + + assert_eq!(seq_number, packet.seq_number()); + assert_eq!(ack_number, packet.ack_number()); + assert_eq!(24, packet.header_len()); + assert_eq!(fin, packet.fin()); + assert_eq!(syn, packet.syn()); + assert_eq!(rst, packet.rst()); + assert_eq!(psh, packet.psh()); + assert_eq!(ack, packet.ack()); + assert_eq!(urg, packet.urg()); + assert_eq!(ece, packet.ece()); + assert_eq!(cwr, packet.cwr()); + assert_eq!(ns, packet.ns()); + + assert_eq!(window_len, packet.window_len()); + assert_eq!(urgent_at, packet.urgent_at()); + assert_eq!(options, packet.options_mut()); + assert_eq!(payload, packet.payload_mut()); + // assert!(packet.verify_checksum(&src_addr.into(), &dst_addr.into())); + assert!(packet.check_len().is_ok()); + } + + #[kani::proof] + fn prove_truncated() { + let packet: Packet> = kani::any(); + let data: &Vec = packet.buffer.as_ref(); + + let trunc_length: usize = kani::any_where(|l| *l < 24); + let packet_in = Packet::new_unchecked(&data[..trunc_length]); + + assert!(packet_in.check_len().is_err()); + } + + #[kani::proof] + fn prove_impossible_length() { + let mut bytes = vec![0; 20]; + let mut packet = Packet::new_unchecked(&mut bytes); + let max_len: u8 = field::URGENT.end.try_into().unwrap(); + let header_len: u8 = kani::any_where(|l| *l < max_len); + packet.set_header_len(header_len); + assert!(packet.check_len().is_err()); + } + + #[cfg(notci)] + #[kani::proof] + #[kani::unwind(15)] + fn prove_repr_invertible() { + // This proof is interesting but too heavy to run frequently on CI. + let repr: Repr = kani::any(); + let mut bytes = vec![0xa5; repr.buffer_len()]; + let mut packet = Packet::new_unchecked(&mut bytes); + + let src_addr: Ipv4Address = kani::any(); + let dst_addr: Ipv4Address = kani::any(); + + repr.emit( + &mut packet, + &src_addr.into(), + &dst_addr.into(), + &ChecksumCapabilities::ignored(), + ); + + let packet_out = Packet::new_unchecked(&packet.into_inner()[..]); + + let repr_out = Repr::parse( + &packet_out, + &src_addr.into(), + &dst_addr.into(), + &ChecksumCapabilities::ignored(), + ); + + assert!(repr_out.is_ok()); + assert_eq!(repr, repr_out.unwrap()); + } + + #[kani::proof] + #[kani::unwind(15)] + fn prove_header_len_multiple_of_4() { + let repr: Repr = kani::any(); + assert_eq!(repr.header_len() % 4, 0); // Should e.g. be 28 instead of 27. + } + + #[kani::proof] + #[kani::unwind(15)] + fn prove_tcpoption_invertible() { + let option: TcpOption = kani::any(); + let buffer = &mut [0; 40][..option.buffer_len()]; + assert_eq!(option.emit(buffer), &mut []); + + let option_out = TcpOption::parse(&*buffer); + assert!(option_out.is_ok()); + assert_eq!(option, option_out.unwrap().1); + } +}