系统软件是控制和协调计算机底层硬件及外部设备、支持应用软件开发和运行的系统核心基础软件，涵盖了操作系统、编程语言、编译器、解释器、数据库、运行时环境、集成开发环境等。随着人工智能、物联网、区块链、系统编程语言、云计算、开源指令集等领域的快速发展，相关系统软件的安全问题大量涌现，比如利用CPU预测执行的Meltdown“熔断”和Spectre“幽灵”攻击、利用软件供应链发起的后门攻击和漏洞攻击...
随着计算机系统在工业和生活中越来越广泛的应用，软件和硬件的可靠性受到越来越多的关注。定理证明方法将程序和系统的正确性表达为数学命题，然后使用逻辑推导的方式证明正确性。不同于基于程序测试的进路，定理证明方法能保证覆盖所有边缘情况，完全排除一个特定类型的错误。而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小的限制，验证非常复杂的系统和性质。因此，定理证明技术不仅是形式化方法领域，也是众...
软件是新一代信息技术的灵魂，是关系国民经济和社会全面发展的基础性、战略性产业。近年来，区块链、云计算、人工智能等许多新兴技术迅速发展，软件工程与工业控制、制造、科学计算、数值计算、物联网等各领域进一步加强融合，正引领并促进这些领域的高速发展。为了满足各个领域的相关要求，软件也对应呈现出许多新的特征，包括计算需求不断增强、实时性和可靠性的要求不断提高、对效率和安全性要求更为严格等等。这些特点导...
形式化方法以严格的数学化和机械化方法为基础来规约、设计、构建、验证、演进计算系统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已成为安全攸关系统质量保障不可或缺的重要载体。 形式化方法己经成功应用于各种硬件设计，特别是芯片的设计。各大硬件制造商都有一个非常强大的形式化方法团队为保障系统的可靠性提供技术支持，例如IBM、AMD等等。近年来，随着形式验证技术和工具的发展，特别是在程序验...
深度学习是人工智能领域的一个新兴技术，近几年获得广泛的关注。深度学习技术已在一些长期未解决的任务取得了与人类相当的能力，比如计算机视觉、自然语言处理、语音识别等。随着技术的长足进步，越来越多的深度学习系统应用随之而生。时至今日，深度学习系统已经被大量用于医药、 金融、交通、国防、电力等行业。然而，目前深度学习系统也同时面临着亟待解决的安全性和可靠性等可信性问题。深度学习系统的可信性已经逐渐成...
Microservice architecture has been the mainstream of cloud native software applications. Nowadays, more and more companies have chosen to migrate from the so-called monolithic architecture to microservice architecture. Industrial microservice systems can be extremely complex. Typically, a large-scale microservice system can include hundreds to thousands of services and is complicated due to the extremely small grained services and their complex interactions and the complex configurations of the runtime environments. Moreover, a microservice system can be highly dynamic:....
