SCAD: Towards a Universal and Automated Network Side-Channel Vulnerability Detection

2 min read

SCAD treats a network side channel as a violation of non-interference: what an off-path attacker observes (a reply or not, or how a reply differs) should not depend on a victim’s secret, such as a port number. Non-interference relates pairs of executions, so SCAD runs selective symbolic execution (on S2E) over a protocol implementation. It makes both packets and protocol state variables symbolic, so it can start from deep states without replaying hundreds of packets, and switches between symbolic and concrete execution to keep the kernel tractable. For each path it records how secrets flow into shared variables and how shared variables shape what the attacker sees, then pairs paths to find violations. The analyst labels secrets and observables and chooses the code to analyse.

Findings

  • On TCP in Linux, FreeBSD and lwIP and UDP in Linux, 48-hour runs report 17 side channels: 14 real, 7 of them previously unknown, a false positive rate of 17.6%.
  • Some new channels reopen patched Linux and FreeBSD kernels to SAD DNS-style or off-path TCP attacks.
  • Setup took about one person-day, against 2.5 person-weeks reported for building the model in SCENT, the model-checking approach. SCENT missed channels because time never advances in its model and because variables are marked by hand.
  • Breadth-first exploration works better than depth-first, since most leaks sit in early error handling. On Linux 4.8 all 6 reports (one a false positive) came within 4.5 CPU hours.

Limits

  • Symbolic state variables can take impossible values (the ICMP credit counter never exceeds 50 in practice, but SCAD allows any 32-bit value). Bad concretisation of such values caused the two false positives in the main table.
  • Needs an expert to define secrets, observables and scope. Open-source stacks only; closed source is left to future work.
  • Finds channels without measuring how much leaks or how fast.

Relevance

Non-interference can be stated for a robot as well: what an attacker can observe after sending a spoofed message should not reveal internal state such as the robot’s plan or its estimate of where it is. Checking that property for a ROS 2 stack is an open problem for robot-security, cyber-physical-security and robust robotics. Follows SAD DNS and its sequel.