近日，beat365手机中文官方网站师生在可信软件安全分析和软件隐私安全领域的两项成果被FSE（ACM International Conference on the Foundations of Software Engineering）2024录用。FSE是软件工程领域的两大旗舰会议之一，也是中国计算机学会（CCF）推荐A类国际会议，截止2024年已举办32届，今年将在巴西召开。

成果1：

论文题目：Finding and Understanding Defects in Static Analyzers by Constructing Automated Oracles

完成人：何为刚、狄鹏、明孟立、张枨宇、苏亭、李世杰

软件静态分析是用于发现软件安全漏洞的一种重要技术手段。然而，静态分析工具的潜在缺陷可能会影响其分析结果的完备性（导致漏报）和精确性（导致误报）。这些分析工具通常缺乏清晰和完整的设计规范，不同分析工具的分析结果也有所不同，因此如何验证静态分析工具的正确性是一项挑战性任务。为此，该成果设计了两种新型的自动化测试预言机制，通过随机生成的程序来寻找静态分析工具中的缺陷。该成果在Clang/LLVM编译器自带的静态分析工具CSA、GCC编译器自带的静态分析工具GSA、和蚂蚁商业静态分析工具Pinpoint中发现了38个此前未知的缺陷，其中28个已经得到开发者的确认或修复。通过对这些发现的缺陷进行案例研究，进一步得到了多项洞察，可改进和更好地理解软件静态分析技术所面临的挑战。

图1：本研究工作提出的两种新型测试预言机制（即动态预言和静态预言机制）

成果2：

论文题目：Property-based Testing for Validating User Privacy-Related Functionalities in Social Media Apps

完成人：孙静翎、苏亭、孙军、李建文、王孟飞、蒲戈光

社交媒体应用软件中有各种与用户隐私安全相关的功能。例如，TikTok用户可以上传视频，并指定哪些用户可以有权限观看这些视频。确保这些隐私功能的正确性至关重要，否则可能会威胁到用户的隐私安全。由于缺乏合适的自动化测试技术，手工测试仍然是业界实践中验证这些功能的主要方法。然而，手工测试往往繁琐、容易出错且不充分。该成果提出了一种基于性质的测试方法，根据给定的隐私规范验证应用行为。这一方法的核心思想是，由测试人员用自然语言编写的隐私规范可以综合生成自动机，该自动机可用于检查应用软件是否已到达不安全状态，从而检测与隐私规范不一致的应用行为。通过与字节跳动的合作，该成果可以有效验证与用户隐私相关的功能，在每次应用发布前平均减少95.2%的手工测试成本。该成果在七个经过广泛测试的社交媒体应用软件（TikTok、西瓜视频、哔哩哔哩、Instagram、Twitter、Threads和Facebook）中依然发现了22个与隐私规范不一致的应用行为（包括4个用户隐私数据泄露、9个与隐私功能错误和9个隐私规范问题）。

图2：本研究工作提出的隐私安全测试技术流程图

上述成果标志着我院师生在软件与系统安全方向取得了新的进展，和头部企业的产学研合作也取得了良好成效。今后课题组也将在编译器、操作系统、网络协议等基础软件与系统安全方向展开更深入研究。

内容来源于课题组

编辑丨单个电子

审核丨曹桂涛 张民