小组五项研究成果被第61届ACM/IEEE DAC 2024接收

Design Automation Conference（DAC）由IEEE与ACM联合主办，是集成电路辅助设计和嵌入式系统领域的国际顶级会议，迄今已有61年的历史，主要关注芯片、电路以及系统设计的新工具和新方法。近几年的接收率为20％左右。DAC是中国计算机学会推荐的A类国际学术会议（CCF-A），是清华大学计算机学科推荐A类会议。本次清华大学软件系统安全保障小组共有5项研究成果被DAC 2024 接收。

第一项研究成果是：Effectively Sanitizing Embedded Operating Systems。该论文主要提出一个可以应用于嵌入式操作系统固件上的Sanitizer工具，即EmbSan。该工具主要解决固件在模糊测试场景下的回调插桩可行性与回调一致的处理难题。EmbSan的主要工作步骤包括提取Sanitizer模板的拦截函数定义及实现，通过自动化或人工方法抽取其初始化流程，根据目标固件的能力定制动态插桩粒度与位置，并在模糊测试时维护运行时信息并将插桩回调进行处理以确定其执行合法性。EmbSan目前已集成于诸多基于Embedded Linux、FreeRTOS、LiteOS于VxWorks的嵌入式固件中。在测试中，EmbSan的运行时开销达到了2.2×到5.7×之间，与现有定制化的Sanitizer工具处于相似水平。与此同时，EmbSan成功在这些固件中发现了41个新的bug。该工作由博士生刘健中、沈煜恒，硕士生徐意如以及毕业硕士生孙浩共同完成。

第二项研究成果是：SPFuzz: Stateful Path based Parallel Fuzzing for Protocols in Autonomous Vehicles。该论文提出了面向自动驾驶车辆协议的SPFuzz，一个基于协议状态路径并行模糊测试的框架。其主要思想是根据协议中不同的状态路径对并行模糊测试任务进行高效划分，从而提升并行模糊测试效率。它的主要步骤包括利用协议的数据和状态模型生成状态路径，根据路径多样性和计算复杂度和将其划分成不同任务，同时均衡不同模糊测试实例之间的工作负载。在四个广泛使用的自动驾驶车辆中的协议（ZMTP、MQTT、DDS和DolP）进行了实验，与Peach的并行模式相比，SPFuzz以2.8X-473.2X的速度实现了相同的代码覆盖率，并发现了6个先前未知的漏洞（5个获得CVE编号）此外，SPFuzz已经适配了NISSAN等几家供应商的ECU，发现了四个导致系统崩溃的缺陷。该工作由硕士生于珺泽，博士生罗正雄，博士后赵艳阳等共同完成。

第三项研究成果是：Efficient Code Generation for Data-Intensive Simulink Models via Redundancy Elimination。该论文提出了Frodo，一个针对数据密集型Simulink模型的高效代码生成器。Frodo的主要思想是识别并消除模型中数据截断型组件导致的冗余运算，进而有效提升生成代码的效率。它的主要步骤包括对模型进行分析得出每个组件的输入/输出映射关系，根据映射关系推到每个组件精确的计算范围，以及为可优化的组件生成精简代码。在广泛应用的模型数据集中，Frodo相比于行业领先工具（Simulink Embedded Coder、DFSynth和HCG），在代码执行效率上提升了1.17-8.55倍。该工作由硕士生喻泽弘，博士后苏卓等共同参与完成。

第四项研究成果是：AccMoS: Accelerating Model Simulation for Simulink via Code Generation。该论文提出了AccMoS，一个基于代码生成的Simulink模型仿真验证框架。AccMoS的主要思想是通过代码生成的方式来加速Simulink中的数据流模型的仿真，以便更快地发现模型中的安全隐患并提高覆盖率，使得模型驱动开发得到的软件更加安全。它的主要步骤包括预处理输入的Simulink模型，针对每个需要收集数据或进行诊断的组件生成相应的仿真功能插桩代码，然后将这些插桩代码与根据模板生成的组件代码以及导入测试用例的代码相结合，合成最终的仿真代码。实验结果表明，AccMoS执行模型仿真的效率比Simulink的模型仿真引擎平均提高了215.3倍，同时能够有效地检测出模型中潜在的缺陷，提高模型驱动开发得到的软件的安全性。该工作由硕士生程一帆、硕士生喻泽宏、博士后苏卓等共同参与完成。

第五项研究成果是：CFTCG: Test Case Generation for Simulink Model through Code Based Fuzzing。该论文提出了CFTCG，一种基于代码模糊测试的Simulink模型测试用例生成方法。首先，CFTCG为模型生成模糊测试代码，其中包括关联模型输入信息的模糊测试驱动程序和带有模型级分支插桩的模型逻辑代码。然后将这些代码编译在一起来执行面向模型的模糊测试循环。在循环过程中，我们利用模型输入端口的字段信息和迭代执行之间的覆盖差异，实现更有针对性的输入数据变异。实验结果表明，与Simulink设计验证器和前沿的学术工作SimCoTest相比，CFTCG在决策覆盖率方面分别平均提高了47%和100%，在条件覆盖率方面分别提高了38%和44%，在MCDC方面分别提高了144%和232%。该工作由博士后苏卓和硕士生喻泽弘等共同参与完成。