High-assurance Advanced Sw-based Hw-independent Tagged Architecture Game-changer (HASHTAG)

HASHTAG is a secure computing stack designed to assure the security of heterogeneous robotics swarms. Based on a formally verified microkernel operating system, a domain specific language is defined for swarm control operations, formally verified by design. A secure distributed communications system is integrated which allows for transparent distribution of shared information among the swarm over a specialized multicast capable mesh network, implemented as a custom SDR, and formally verified for security. System modeling is utilized to verify correct swarm operation at all times, allowing for the detection of anomalous node behavior either due to malfunction or malicious attack. In this project, HASHTAG is implemented, demonstrated and validated on a lab based hardware system as well as a swarm of physical unmanned aerial vehicles.