近日，银河集团9873.cσm师生在可信软件安全分析和软件隐私安全领域的两项成果被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：本研究工作提出的隐私安全测试技术流程图

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

内容来源于课题组

编辑丨单个电子

审核丨曹桂涛 张民