Biblio

MQTT is widely adopted by IoT devices because it allows for the most efficient data transfer over a variety of communication lines. The security of MQTT has received increasing attention in recent years, and several studies have demonstrated the configurations of many MQTT brokers are insecure. Adversaries are allowed to exploit vulnerable brokers and publish malicious messages to subscribers. However, little has been done to understanding the security issues on the device side when devices handle unauthorized MQTT messages. To fill this research gap, we propose a fuzzing framework named ShadowFuzzer to find client-side vulnerabilities when processing incoming MQTT messages. To avoiding ethical issues, ShadowFuzzer redirects traffic destined for the actual broker to a shadow broker under the control to monitor vulnerabilities. We select 15 IoT devices communicating with vulnerable brokers and leverage ShadowFuzzer to find vulnerabilities when they parse MQTT messages. For these devices, ShadowFuzzer reports 34 zero-day vulnerabilities in 11 devices. We evaluated the exploitability of these vulnerabilities and received a total of 44,000 USD bug bounty rewards. And 16 CVE/CNVD/CN-NVD numbers have been assigned to us.

Commodity I/O hardware often fails to separate I/O transfers of isolated OS and applications code. Even when using the best I/O hardware, commodity systems sometimes trade off separation assurance for increased performance. Remarkably, device firmware need not be malicious. Instead, any malicious driver, even if isolated in its own execution domain, can manipulate its device to breach I/O separation. To prevent such vulnerabilities with high assurance, a formal I/O separation model and its use in automatic generation of secure I/O kernel code is necessary.This paper presents a formal I/O separation model, which defines a separation policy based on authorization of I/O transfers and is hardware agnostic. The model, its refinement, and instantiation in the Wimpy kernel design, are formally specified and verified in Dafny. We then specify the kernel implementation and automatically generate verified-correct assembly code that enforces the I/O separation policies. Our formal modeling enables the discovery of heretofore unknown design and implementation vulnerabilities of the original Wimpy kernel. Finally, we outline how the model can be applied to other I/O kernels and conclude with the key lessons learned.