Apple kernel Driver Analyzer

We developed the first automatic, program-analysis tool called iDEA for analyzing Apple kernel drivers (C++ binaries without symbols/source code). See the full 15K lines of source code on Github.

iDEA enabled the first large-scale study of 3,400 Apple driver binaries across 15 OS versions of iOS, tvOS, iPadOS, and macOS, and discovered 35 zero-day bugs. Also see our CCS'20 paper.

Secure MQTT Server

We released a secure implementation of MQTT server (based on Eclipse Mosquitto) enhanced with the MOUCON access control model proposed in our Oakland'20 paper. MQTT is the most widely used IoT messaging protocol in the modern, cloud-based IoT architecture (e.g., AWS IoT, Asure IoT). See the source code on Github.  

Model Checker for IoT delegation protocols

We released the source code of the first model checker, named VerioT, that is capable of semi-automatic, scalable modeling check for heterogeneous IoT delegation protocols in the wild (e..g, those developed by IoT vendors SmartThings, Philips, Google, IFTTT, LIFX). See the six design flaws found by VefioT in our Usenix Security'20 paper.