Home

中心汪宇霆教师团队在机器代码验证方向取得研究进展


  • 2021-06-02 11:43:52

      近日,上海交通大学约翰·霍普克罗夫特计算机科学中心(以下简称“中心”)长聘教轨副教授汪宇霆团队在理论计算机领域机器代码验证研究方向取得重要进展,相关成果“Automatic Generation and Validation of Instruction Encoders and Decoders”已被计算机科学理论领域顶级会议The 33rd International Conference on Computer-Aided Verification(CAV2021)接收,汪宇霆为通讯作者。值得一提的是,团队成员均为本科生。该研究基于汪宇霆指导的第38期上海交通大学PRP(Participation in Research Program)项目“指令编码及译码的形式化研究”。

       CAV是计算机科学理论领域的顶级会议之一,也是中国计算机协会(CCF)推荐A类会议。该会议致力于硬件和软件系统的计算机辅助形式化分析方法的理论和实践的进步,涵盖从实用的验证工具以及实现这些工具所需的算法和技术。CAV每年以中国科研机构为第一单位的论文仅2-3篇。

      机器指令的编码和译码是操作机器代码的软件(如编译器)中的重要一环。这些软件的正确性依赖于编码器和译码器的一致性(Consistency),即编码和译码互为逆过程。已有的相关研究依赖于带二义性(Ambiguity)的指令规范,并不能从根本上保证这一关键性质成立,这成为了机器代码验证相关研究方向的一个关键瓶颈。

       汪宇霆团队注意到由于指令译码的确定性,指令结构中天然地包含着可以生成一致性编码器译码器的信息。基于这些观察,该团队开发了一套框架,其从精确的指令规范出发,自动生成编码器和译码器以及它们的一致性证明,从逻辑层面完整保障了编码译码过程的正确性。

      具体来说,在这个框架中,开发了名为Core-SLED (Core Specification Language for Encoding and Decoding)的规范语言以精确描述指令格式,以及一系列C++算法来解释用户输入的指令规范文件,最终输出用Coq编写的编码器译码器及证明(Coq是一个广泛使用的交互式定理证明器)。汪宇霆团队已经成功的将该框架应用于x86指令集的一个关键子集。

       该工作解决了如何自动生成一致的、经过验证的编码器和译码器这一重要开放问题,不仅为操作机器代码的可信软件的进一步发展扫清了关键障碍,且对推动形式化指令集(Formalized Instruction Set Architectures)研究的进步有着重大意义。

© John Hopcroft Center for Computer Science, Shanghai Jiao Tong University
分享到

地址:上海市东川路800号上海交通大学软件大楼专家楼
邮箱:jhc@sjtu.edu.cn 电话:021-54740299
邮编:200240