Crystal (ball): I Look at Physics and Predict Control Flow! Just-Ahead-Of-Time Controller Recovery

Recent major attacks against unmanned aerial vehicles (UAV) and their controller software necessitate domain-speciic cyber-physical security protection. Existing oline formal methods for (untrusted) controller code veriication usually face state-explosion. On the other hand, runtime monitors for cyber-physical UAVs often lead to too-late notiications about unsafe states that makes timely safe operation recovery impossible. We present Crystal, a just-ahead-of-time control low predictor and proactive recovery for UAVs. Crystal monitors the execution state of the light controller and predicts the future control lows ahead of time-based on the UAV’s physical dynamics. Crystal deploys the operator’s countermeasures proactively in case of an upcoming unsafe state. Crystal’s just-ahead-of-time model checking explores the future control lows in parallel ahead of the UAV’s actual operation by some time margin. The introduced time margin enables Crystal to accommodate operator’s feedback latency by the time the actual execution reaches to the identiied unsafe state. Crystal periodically queries the controller’s execution state. It emulates the UAV physical dynamical model and predicts future sensor measurements (controller inputs) and upcoming feasible controller’s execution paths. This drives Crystal’s model-checking exploration away from unreachable future states. Crystal’s selective model checking saves computational time to stay ahead of execution by concentrating on relevant upcoming control lows only. This eliminates the state-explosion problem in traditional oline formal methods. We evaluated a multi-threaded prototype of Crystal between the control station server and the UAV. Crystal was able to predict upcoming hazardous states caused by the thirdparty controller program and proactively restored the safe states successfully with minimal overhead.