信息物理系统软件设计自动化专题前言

为了更精确地认识与改造世界，新一代的嵌入式系统必须将计算世界与物理世界作为紧密交互的整体进行认知，实现集计算、通信与控制于一体的深度融合的理论体系与技术框架，即信息物理系统（cyber-physical systems，简称CPS）.与传统嵌入式系统不同，CPS充分考虑了计算部件与物理环境的深度融合，通过将设备智能化连接，实现物理环境系统与计算系统之间精确感知与高效协同.基于CPS理念设计出来的计算设备可以根据具体任务需求自适应地调整与配置计算逻辑，精确智能地获取外部物理环境信息并做出针对性的实时反应，完成安全可靠的控制服务，从而实现物理世界与信息世界的有机统一.
随着人们对信息技术质量要求的不断提高，CPS迅速在众多安全攸关领域得以部署承担关键任务.从远程精准医疗到智能轨道交通，从无人驾驶到航空航天，从智慧城市到智能制造，无处不见CPS的身影.虽然CPS在众多领域获得成功，然而由于其涉及多维时空约束、异构物理/计算进程交互、运行环境不确定等因素，CPS设计复杂度极高.在缺乏设计自动化方法与技术的情况下，CPS开发周期长且质量难于保证.日益复杂的CPS设计与实现在给产业界与学术界带来巨大挑战的同时，也创造了大量新的机遇，CPS设计自动化目前已成为国际相关研究领域的关注与研究热点.
本专题采取自由投稿的方式，共收到14篇投稿.特约编辑邀请了30余位领域专家参与审稿，每篇稿件至少邀请3位专家进行评审，每篇录用稿件都经过至少3轮审稿.14篇稿件中共计10篇稿件通过第1轮评审，8篇稿件通过第2轮评审，并在CCF软件工程专业委员会、系统软件专业委员会年会全国软件与应用学术会议NASAC2019会议上进行了报告.经过第3轮终审及少数稿件的第4轮复审后，最终有6篇论文入选本专题.
《基于SHML的CPS行为建模及仿真》提出了一种面向CPS领域的建模及仿真方法，设计并实现了一个集成的面向CPS行为的建模与仿真平台，为CPS的建模及仿真提供了一种有效的方法及工具支撑.
《垂悬指针检测与防御方法》针对复杂系统软件中广泛出现的悬垂指针问题进行研究，提出了一种名为DangDone的垂悬指针防御方法，通过在编译时的程序转换来定位潜在的垂悬指针并防御use-after-free或double-free漏洞.
《自主机器人多智能体软件架构及伴随行为机制》提出了基于多智能体的自主机器人控制软件软件架构，以及基于相应架构的伴随行为机制.该工作基于分步规划和动态决策的思想设计并实现了相应自主决策算法DAAB，并在相应仿真环境和实际机器人环境上进行了案例分析.
《轨道交通联锁领域特定语言的形式化》基于轨道交通联锁系统中故障的随机性和行为实时性的特点，提出了基于建立随机混成系统模型来仿真、预测轨道交通连锁系统的方法.该方法在实际联锁系统进行实例研究，并在UPPAAL-SMC平台上进行了事故模型的预测分析.
《基于AADL的失效概率分配及安全性评估方法》综合考虑AADL架构的层次化设计、模型复杂度和构件失效造成影响的严重程度，针对安全关键系统提出基于AADL的失效概率分配方法，以应对安全性评估过程中如何分配失效概率的问题.相关技术在飞控CPS系统上进行了实例研究.
《马尔可夫信息物理系统拒绝服务攻击安全控制》研究了马尔可夫跳变信息物理系统在模态依赖拒绝服务（DoS）攻击下的安全控制问题.提出了一种新颖的模态依赖事件触发策略来减少网络资源消耗.
本专题面向信息物理系统的研究人员和工程人员，内容涵盖系统建模、系统架构、可信保障等领域，反映了我国学者在相关领域的高水平研究成果.感谢《软件学报》编委会、CCF软件工程专委会、系统软件专委会对专题工作的指导和帮助，感谢专题全体评审专家及时、耐心、细致的评审工作，感谢踊跃投稿的所有作者.希望本专题能够对形式化方法的科研工作有所促进.
专刊特约编辑、北航计算机学院刘超教授在专刊的筹划阶段分享了大量宝贵的经验，并在征稿、审稿等环节做了大量的工作，使得专刊实施过程得以顺利开展.然而，在本专刊即将完成之际，刘超老师却因病永远离开了我们.刘老师睿智、谦逊、渊博、平和，为推动我国软件工程事业发展做出了重要贡献，我们借此表达深深的怀念和敬意.
     

基于控制流的代码混淆技术研究

为了提高基于垃圾代码的控制流混淆方法的优化效果, 针对插入分支垃圾代码以及循环垃圾代码会引入大量额外开销的问题, 从软件保护中代码混淆技术出发, 对代码混淆技术的研究现状和原理、混淆算法攻击以及基于控制流混淆技术作了深入研究, 提出一种基于Java代码控制混淆中插入垃圾代码的改进方法。新方法与基于垃圾代码的控制流混淆变换方法比较, 结果表明, 新方法增加了代码抵抗攻击者的静态分析的能力, 增加了反编译以及逆向工程的难度, 既达到了很好的防御逆向工程攻击的效果, 又不会大量引入额外的系统开销。     

EBound:一种高效的空间内存错误检测方法

空间内存错误是C语言程序中经常出现的一种漏洞。针对目前空间内存错误检测方法的性能开销高的问题,提出一种高效的空间内存错误检测方法 EBound。EBound使用动态指针边界检测方法检测程序中的空间内存错误,并使用静态污点分析方法来消除不必要的指针边界检查,从而降低了性能开销。EBound基于LLVM编译器实现,不需要对程序源代码进行修改。实验结果表明,EBound可以有效地防御利用空间内存错误进行的缓冲区溢出攻击。与当前比较好的空间内存错误检测方法 Soft Bound相比,EBound有更低的性能开销。     

MTD增强的网络欺骗防御系统

计算机网络正在飞速发展,但随之而来的系统破坏、信息泄露等网络安全问题也日益突出。攻击者在正式攻击前通常进行大量的网络侦查,以发现目标网络和系统上的可利用漏洞,而传统网络系统中的静态配置为攻击者发现网络目标和发起攻击提供了极大的优势。为了减轻攻击者持续性网络侦查攻击的有效性,基于软件定义网络开发了移动目标防御（moving target defense,MTD）增强的网络欺骗防御系统。该系统采用网络欺骗技术,混淆攻击者收集到的目标网络和系统信息,延长攻击者扫描到网络内真实脆弱性主机的时间,提高其时间成本;并在此基础上融合移动目标防御技术,动态随机地变换网络内节点的IP地址,增强网络欺骗系统的防御效能。实现了系统原型并对其进行评估,在虚拟网络拓扑规模为3个网段且地址变换周期为30 s的配置下,该系统将攻击者发现脆弱性主机的时间平均延迟7倍,将攻击者成功攻击脆弱性主机的概率降低83%,同时系统额外开销平均在8%以内。     

一种基于运行时信息的以太坊智能合约防御技术

智能合约是区块链技术最成功的应用之一,已经被广泛集成到应用程序中,成为应用去中心化的常见实现方案.然而,智能合约由于其独有的金融特性,一直以来饱受安全攻击,各种新的恶意攻击类型层出不穷.现有的研究工作提出了多种有效检测合约漏洞的方法,但在实际应用中都存在着各种局限:仅针对已知的漏洞类型,需要修改合约代码来消除漏洞,链上开销过大.由于智能合约部署到链上后的不可修改性,这些针对特定漏洞类型的检测防御手段无法对原有的合约进行修复,因此很难及时地应对新型的漏洞和攻击.为此,提出了一种基于运行时信息的智能合约可升级防御技术,通过引入运行时的各种信息,为链下对攻击和漏洞的检测提供实时的数据.同时,设计了一套部署在合约上的访问控制机制,基于动态检测的结果,对合约的访问进行限制,从而在不需要修改合约代码的情况下实现动态的防御.由于以太坊本身的机制无法对实时攻击进行识别和拦截,为了减小这一影响,利用竞争(race condition)的机制来增强防御的效果.实验结果分析表明:该防御技术可以有效地检测并防御攻击,对于后续的攻击交易,可以实现100%的拦截成功率,对于首次检测到的实时攻击,利用竞争可以达到97.5%的成功率.     

基于S2E的Use-After-Free漏洞检测方案

Use-After-Free漏洞是由程序试图操作悬垂指针引起的。该类型漏洞近年来在针对浏览器客户端的攻击中变得愈发流行。提出一种针对Use-After-Free漏洞的检测算法,并据此实现检测方案UAFChecker。UAFChecker基于开源的多路径软件分析平台S2E,它通过挂钩关键的堆内存操作函数监控指针的生成,使用反汇编引擎BeaEngine在汇编层上跟踪指针的传播,通过收集和分析指针信息来检测漏洞。实验结果表明,配合Fuzzing技术UAFChecker成功定位和分析出IE8浏览器中存在的多个未被公开的Use-After-Free漏洞。     

拟态防御体系攻击检测研究与分析

网络空间拟态防御技术是一种采用动态异构冗余架构的新型主动防御技术,论述了基于拟态防御体系的攻击检测方法,能够检测定位漏洞并及时修复,完成从静态防御到动态防御的转变,提高对未知漏洞和后门攻击的防御能力。     

拟态防御Web服务器设计与实现

Web服务器系统作为重要的服务承载和提供平台,面临的安全问题日益严重.已有的防御技术主要基于已知攻击方法或漏洞信息进行防御,导致难以很好地应对未知攻击的威胁,从而难以全面防护web服务器系统的安全.论文首先提出了攻击链模型,对已有技术的问题和不足进行了深入的分析.在此基础上,提出了基于“动态异构冗余”结构的拟态防御模型,并描述了拟态防御模型的防御原理和特点.基于拟态防御模型构建了拟态防御web服务器,介绍了其架构,分析了拟态原理在web服务器上的实现.安全性和性能测试结果显示拟态防御web服务器能够在较小开销的前提下,防御测试中的全部攻击类型,说明拟态防御web服务器能够有效提升系统安全性,验证了拟态防御技术的有效性和可行性.最后讨论了拟态防御技术今后的研究前景和挑战.     

ARM指针认证机制研究综述

内存错误漏洞是以不安全语言编写软件系统中安全性和可靠性问题的主要原因。这些漏洞常被用来将代码执行重定向到攻击者控制的位置。诸如代码复用攻击这样的内存错误漏洞利用的流行促使主要处理器制造商设计基于硬件的防御机制。一个例子是ARMv8.3中引入的指针认证(PAuth)机制。PAuth使用签名密钥和指针上下文信息对指针进行签名, 上下文信息是缩小保护范围和开发不同类型安全机制的关键元素。通过使用轻量级分组密码算法QARMA64并将指针认证码(PAC)存储在指针未使用位中, PAuth可以较小的性能和存储开销检查指针的完整性。当前一些研究使用PAuth降低内存安全机制的性能开销, 还有一些研究基于PAuth提高控制流完整性的保护精度。虽然PAuth受到越来越多的关注, 但它仍然遭受暴力攻击和PAC伪造攻击。因此, 很有必要对当前基于PAuth的安全应用进行总结, 并分析其存在的问题。本文首先介绍内存错误漏洞利用的相关背景和相应的保护机制。然后, 我们详细介绍了PAuth机制的详细信息, 包括硬件支持、加密算法和密码密钥管理, 及其潜在的安全问题。然后, 我们总结了当前基于PAuth的内存安全和控制流完整性的研究, 特别是指针上下文的选择方法。最后, 基于我们的调查, 讨论和展望ARM PAuth未来可能的研究方向。未来的研究方向可能包括以下几个方面: PAuth密钥管理和上下文选择、针对推测攻击的防御, 以及PAuth与其他ARM安全机制的结合使用。     

PEC-V: 基于RISC-V协处理器的内存溢出防御机制

内存溢出攻击是计算机系统中历史悠久且依旧广泛存在的攻击手段,而指针加密技术可以有效阻止此攻击.通过软件手段实现这一技术的方式将导致程序运行效率的显著降低并且产生额外的内存开销.所以本文基于RocketChip的RoCC(Rocket Custom Coprocessor)接口实现一个加解密指针的协处理器PEC-V.其通过RISC-V的自定义指令控制协处理器加解密返回地址和函数指针等值达到阻止溢出攻击的目的.PEC-V主要使用PUF(Physical Unclonable Function)来避免在内存中储存加密指针的键值,所以此机制在保证了加密键值的随机性的同时也减少了访问内存的次数.实验结果显示,PEC-V能够有效防御各类缓冲区溢出攻击,且程序平均运行效率仅下降3％,相对既往方案显著提高了性能.     

Making Pointers Safe in System Programming Languages

System programming languages usually provide pointers so as to permit efficient and understandable programs to be written. Some higher level languages either avoid pointers altogether or greatly circumscribe pointers to guarantee safety, i.e., so that programs cannot gain access to storage in an inappropriate way. By combining the ideas of 1) pointer scope front Algol 68, 2) tombstones for invalidating dangling references, and 3) freezing which permits freeable objects to have scoped pointers, we solVe the problem of providing convenient and efficient pointers while simultaneously guaranteeing safety.     

The implementation of generic smart pointers for advanced defensive programming

Smart pointers denote a well‐known technique for collective resource ownership, e.g. sharing dynamic object instances, while usually supporting automatic garbage collection based on reference counting. The original method has been retargeted to serve as a generic defensive programming method for ‘exhaustive tracking’ of erroneous pointer use in C++. Automatic bug tracking is supported in a unified manner both for pointers to heap memory, i.e. free storage, as well as for pointers to stack or global memory, i.e. auto or static storage. Overall, the presented technique (a) offers a simple contract for memory allocation and use; (b) supports type and indirection depth genericity; (c) implements most operators supported for built‐in pointers with embedded bug defense; (d) offers an alternative way of employing a garbage collection facility for memory leak detection; and (e) provides an appropriate collection of utility macros, through which defensive pointers should be used, with an alternative version re‐targeted to normal native pointers. Copyright © 2004 John Wiley & Sons, Ltd.     

Precise Call Graphs for C Programs with Function Pointers

The use of pointers presents serious problems for software productivity tools for software understanding, restructuring, and testing. Pointers enable indirect memory accesses through pointer dereferences, as well as indirect procedure calls (e.g., through function pointers in C). Such indirect accesses and calls can be disambiguated with pointer analysis. In this paper we evaluate the precision of one specific pointer analysis (the FA pointer analysis by Zhang et al.) for the purposes of call graph construction for C programs with function pointers. The analysis is incorporated in a production-strength code-browsing tool from Siemens Corporate Research in which the program call graph is used as a primary tool for code understanding.The FA pointer analysis uses an inexpensive, almost-linear, flow- and context-insensitive algorithm. To measure analysis precision, we compare the call graph constructed by this analysis with the most precise call graph obtainable by a large category of existing pointer analyses. Surprisingly, for all our data programs the FA analysis achieves the best possible precision. This result indicates that for the purposes of call graph construction, inexpensive pointer analyses may provide precision comparable to the precision of expensive pointer analyses.     

二维逻辑PPTLSL的可满足性检查

由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTLSL是一种二维(时间和空间)时序逻辑,它结合了分离逻辑(Separation Logic)与命题投影时序逻辑PPTL(Propositional Projection Temporal Logic),能够描述和验证操作链表的指针程序的时序性质.本文简要回顾了PPTLSL的相关理论,并详细介绍工具SAT-PPTLSL的工作原理.该工具主要利用PPTLSL与PPTL之间构建起来的“同构”关系进行PPTLSL公式的可满足性检查.此外,本文结合一些实例展示了SAT-PPTLSL的执行过程,并通过实验分析了关键参数对SAT-PPTLSL执行效率的影响.     

C＋＋对象的持久化中的问题和解决方案

多媒体智能数据库系统ＭＩＤＳ（ｍｕｌｔｉｍｅｄｉａｉｎｔｅｌｌｉｇｅｎｔｄａｔａｂａｓｅｓｙｓｔｅｍ）是一个对象数据库管理系统．它的数据库编程语言是Ｐ＋＋，Ｐ＋＋个语言是一种基于Ｃ＋＋的语言．作者在Ｐ＋＋的实现过程中遇到了以下问题：首先，Ｃ＋＋的指针有二义性，它无法在语义上区分成员指针和引用指针，以及易失性指针和持久性指针，从而给事务管理中的对象加锁及其它方面带来问题．其次，具有虚拟函数或虚拟基类的对象中含有指向内存中的指针，而这些指针不是由程序员定义的．如果Ｃ＋个对象被持久化，这些指针在不同的程序调用中有可能无效．最后，如果作者用文件系统调用来存储对象，那么必须要设计复杂的Ｃａｃｈｅ系统和做大量对象的格式转化工作，这需要大量的空间和时间，所以他们采用了另外的一种方法──基于虚拟内存空间映射的存储方案．     

Object protection in distributed systems

With reference to a distributed system consisting of nodes connected by a local area network, we consider a salient aspect of the protection problem, the representation of access permissions and protection domains. We present a model of a protection system supporting typed objects. Possession of an access permission for a given object is certified by possession of an object pointer including the specification of a set of access rights. We associate an encryption key with each object and a password with each domain. Object pointers are stored in memory in a ciphertext form obtained by using the object key and including the value of the domain password. Each process is executed in a domain and can take advantage of a given object pointer only if this object pointer was encrypted by including the password of this domain. A set of protection primitives makes it possible to use object pointers for object reference and to control the movements of the objects across the network. The resulting protection environment is evaluated from a number of salient viewpoints, including ease of access right distribution and revocation, interprocess interaction and cooperation, protection against fraudulent actions of access right manipulation and stealing, storage overhead, and network traffic.     

2LP: A double-lazy XML parser

XML is acknowledged as the most effective format for data encoding and exchange over domains ranging from the World Wide Web to desktop applications. However, large-scale adoption into actual system implementations is being slowed down due to the inefficiency of its document-parsing methods. The recent development of lazy parsing techniques is a major step towards improving this situation, but lazy parsers still have a key drawback—they must load the entire XML document in order to extract the overall document structure before document parsing can be performed. We have developed a framework for efficient parsing based on the idea of placing internal physical pointers within the XML document that allow the navigation process to skip large portions of the document during parsing. We show how to generate such internal pointers in a way that optimizes parsing using constructs supported by the current W3C XML standard. A double-lazy parser (2LP) exploits these internal pointers to efficiently parse the document. The usage of supported W3C constructs to create internal pointers allows 2LP to be backward compatible—i.e., the pointer-augmented documents can be parsed by current XML parsers. We also implemented a mechanism to efficiently parse large documents with limited main memory, thereby overcoming a major limitation in current solutions. We study our pointer generation and parsing algorithms both theoretically and experimentally, and show that they perform considerably better than existing approaches.     

指针的学习与应用

指针是C程序设计的重点和难点，也是软件界的讨论热点：、正确而灵活地运用指针，可以有效地表示复杂的数据结构，能动态分配内存，直接处理内存地址等。在学习和应用指针过程中，传统的指针概念和用法常常使人感到困惑。文中提出了单星指针、双星指针等新概念，比较全面地介绍了指针的理论和应用．     

Exploit-oriented Automated Information Leakage

Automatic Exploit Generation (AEG) has become one of the most important ways to demonstrate the exploitability of vulnerabilities. However, state-of-the-art AEG solutions in general assume the target system has no mitigations deployed, which is not true in modern operating systems since they often deploy mitigations like Data Execution Prevention (DEP) and Address Space Layout Randomization (ASLR). This paper presents the automatic solution EoLeak that can exploit heap vulnerabilities to leak sensitive data and bypass ASLR and DEP at the same time. At a high level, EoLeak analyzes the program execution trace of the Proof-Of-Concept (POC) input that triggers the heap vulnerabilities, characterizes the memory profile from the trace, locates sensitive data (e.g., code pointers), constructs leakage primitives that disclose sensitive data, and generates exploits for the entire process when possible. We have implemented a prototype of EoLeak and evaluated it on a set of Capture The Flag (CTF) binary programs and several real-world applications. Evaluation results reveal that EoLeak is effective at leaking data and generating exploits.