The project aims to develop control systems for ground vehicles that are resilient to a variety of external attacks. Our approach is to combine control-level techniques and code-level techniques, resulting in the approach comprises of two major stages: control law design and control task synthesis. Control-level defenses address attacks on the environment of the controller, such as attacks on sensors, actuators, communication media (i.e., the network) and computational resources available to the controller. Our work on control-level defenses builds upon ways to introduce redundancy within the control loop, as well as new methods for detection and identification of attacks. We utilize security-aware estimators that identify an attack and allow the controller to pursue a mitigation strategy. Code-level defenses prevent injection of malicious code into the operation of the controller itself, achieved through verified code generation of control task code. The verification approach is embedded of the code generation algorithm into the Coq proof assistant.
