RQ1: Accuracy

Automated Specification Generation

To evaluate HAFuzz's accuracy, we conducted a comparative experiment against MEDIC, the state-of-the-art baseline for HA-IoT verification.  MEDIC takes IFTTT rules as input and employs automated specification generation using predefined formal templates. It automatically generates CTLs like  AG! (d.st.trust=untrusted & d.st=True). To enable a direct comparison, we modified it to produce LTL formulae with similar natural language meaning, for example, G! (d.st.trust=untrusted & d.st=True), and implemented the same generation method within HAFuzz. Among them, d.st denotes a device state tuple (comprising both device name and state), and each tuple is assigned a trust/privacy attribute. The security issues are categorized into three types:
1. unauthorized access (e.g., Window.Open,  Garage Door.Open and Door.Unlock)
2. financial loss (e.g., Online Banking.Transferring, airconditioner.On and Water Heater.On)
3. privacy leakage (e.g.,Twitter.Posting and Facebook.Posting)
For any IFTTT rule involving devices or services associated with these categories, both tools will automatically generate related specifications. Consider the following IFTTT rules: 

IF Temperature Sensor.temperature > 30 & Motion Detector.motion = active THEN Air Conditioner.cool

IF Gas Sensor.gas > 60 THEN Alarm.both

IF Humidity Sensor.humidity < 20 THEN Humidifier.on

IF Swimming Pool Water Quality Sensor.waterQuality > 60 THEN Swimming Pool Water Pump.on

IF Home Mode.Mode = sleep THEN Window.close & Light.off & TV.off

The tools detects the window device in the final rule and generates the corresponding LTL specification: 

    G! (window.WindowState=open & window.trust_WindowState_open=untrusted)
Table 1 (in the paper) summarizes the total number of all generated specifications and those violated.