2021年2月,浙江大学网络空间安全学院的论文“CSim2: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee”发表于《ACM Transactions on Programming Languages and Systems》(TOPLAS)期刊上,浙江大学为通讯作者单位,这也是TOPLAS期刊自1979年创刊以来,浙江大学首次在该期刊上发表论文。此前,大陆研究机构在TOPLAS期刊以第一(通讯)作者单位仅发表过5篇论文。TOPLAS是计算机程序语言领域的顶级国际期刊,仅接收在原创性、基础性方面有突出贡献的成果,也是中国计算机学会推荐软件工程/系统软件/程序设计语言领域的A类期刊,平均每年刊出论文仅20多篇。
针对工业级多核、并发形态的系统软件,开展代码级的安全性和正确性验证是一直以来的技术难题,该论文以数理逻辑为基础,提出并实现了一种形式化的并发系统编程语言及验证方法,解决了并发安全验证和并发系统自顶向下逐层开发的相关理论问题,研制了原型工具,可应用到操作系统以及区块链、无人车、航空/航天等关键领域基础软件中。
浙江大学网络空间安全学院已经在在物联网安全、系统安全、数据安全、区块链安全、人工智能安全、网络安全等方向取得了丰硕的研究成果,在网络空间安全领域国际顶级期刊(如 IEEE/ACM Transactions TDSC、TIFS、ToN、TISSEC 等)和顶级会议(如 IEEE S&P、ACM CCS、USENIX Security、SIGCOMM、NDSS、IEEE INFOCOM 等)发表论文近百篇,获得11项杰出论文奖。此次论文是浙江大学网安学院与新加坡南洋理工大学网络空间安全实验室共同合作的成果,是浙大网安在编程语言安全方向取得的新突破。此前,双方已经在形式化安全技术、操作系统安全等方向开展了多年的深度合作,共同在形式化验证国际顶级会议和网络安全国际顶级期刊上联合发表多篇有影响力的学术论文。