首页期刊导航|计算机研究与发展
期刊信息/Journal information
计算机研究与发展
计算机研究与发展

徐志伟

月刊

1000-1239

crad@ict.ac.cn

010-62620696;62600350

100190

北京中关村科学院南路6号

计算机研究与发展/Journal Journal of Computer Research and DevelopmentCSCD北大核心CSTPCDEI
查看更多>>本刊是中国科学院计算技术研究所和中国计算机学会联合主办、科学出版社出版的学术性刊物、中国计算机学会会刊，我国第一个计算机刊物。主要刊登计算机科学技术领域高水平的学术论文、最新科研成果和重大应用成果。
正式出版
收录年代

    前言

    卜磊陈振邦
    225-226页
      原文链接:
    • NETL
    • NSTL
    • 万方数据

    抽象解释及其应用研究进展

    陈立前范广生尹帮虎王戟...
    227-247页
    查看更多>>摘要：抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论.抽象解释自20世纪70年代提出以来,在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用.近年来,抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展.基于此,系统综述了抽象解释及其应用的研究进展.首先概述了抽象解释理论的基本概念,介绍了抽象解释理论、抽象域的研究进展;然后概述了基于抽象解释的程序分析方面的研究进展;之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展;又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用进展进行了介绍;最后指明了抽象解释未来可能的研究方向.

    抽象解释程序语义程序分析形式验证抽象域

      原文链接:
    • NETL
    • NSTL
    • 维普
    • 万方数据

    基于多线程并行的符号执行引擎设计与实现

    周彭左志强
    248-261页
    查看更多>>摘要：符号执行作为一种高效的测试生成技术,被广泛应用于软件测试、安全分析等领域.然而,由于程序中的执行路径数量随着分支数量的增加而指数级上升,符号执行往往无法在大规模程序上进行高效执行,缺乏可扩展性.已有的基于多进程的并行化方法具有较大的额外通信开销,并且缺乏对现有约束求解优化技术的利用.提出了基于多线程并行处理模型的符号执行加速方法.具体来讲,为解决并行符号执行中的不同工作节点负载不平衡问题,设计了不需要中间节点参与的工作窃取算法.为充分利用现有约束求解优化技术,提出了让不同工作节点共享约束求解信息的加速求解方法.基于符号执行引擎(KLEE)实现了多线程并行化符号执行方案,从而形成多线程并行化符号执行引擎(PKLEE).实验验证表明,在穷尽执行路径场景下,KLEE平均耗时是在给定8个线程下PKLEE的3～4倍;在同样的时间内,PKLEE执行的有效工作负载平均是KLEE的3倍.

    符号执行负载均衡约束求解并行加速可扩展性

      原文链接:
    • NETL
    • NSTL
    • 维普
    • 万方数据

    模糊测试中的静态插桩技术

    王明哲姜宇孙家广
    262-273页
    查看更多>>摘要：模糊测试是一种行之有效的软件缺陷检测方法.其基本思想是生成大量随机输入,从而广泛探索程序行为,并以此发现程序崩溃和崩溃背后的软件缺陷.显然,纯随机的输入无法高效探索程序行为,大量程序缺陷也难以导致崩溃.为了进一步提升模糊测试的有效性,模糊测试往往引入静态插桩技术,用于加快探索程序状态空间速度,提升发现缺陷的能力.因此,引入静态插桩已经成为当下模糊测试的经典实践.聚焦于模糊测试场景下的插桩需求,除了介绍静态插桩技术的基本原理外,从安全特性强化和导向信息收集两个视角出发,系统性地分析了当下静态插桩的典型方法.同时,针对插桩的额外开销问题,全面地测量了不同插桩方案下的程序的执行速度,并与基线的未插桩程序进行比对.最后基于上述分析和测量,初步展望了静态插桩的优化方向.

    静态插桩模糊测试软件缺陷程序分析额外开销

      原文链接:
    • NETL
    • NSTL
    • 维普
    • 万方数据

    Java指针分析综述

    谭添马晓星许畅马春燕...
    274-293页
    查看更多>>摘要：近年来静态程序分析已成为保障软件可靠性、安全性和高效性的关键技术之一.指针分析作为基础程序分析技术为静态程序分析提供关于程序的一系列基础信息,例如程序任意变量的指向关系、变量间的别名关系、程序调用图、堆对象的可达性等.介绍了Java指针分析的重要内容:指针分析算法、上下文敏感、堆对象抽象、复杂语言特性处理、非全程序指针分析,特别是对近年来指针分析的研究热点选择性上下文敏感技术进行了梳理和讨论.

    指针分析别名分析Java静态分析上下文敏感

      原文链接:
    • NETL
    • NSTL
    • 维普
    • 万方数据

    中断驱动型航天嵌入式软件原子性违反检测方法

    于婷婷李超王博祥陈睿...
    294-310页
    查看更多>>摘要：嵌入式软件的可信性对航天任务的成败至关重要.航天嵌入式软件广泛采用中断驱动的并发机制,不确定的中断抢占可能导致并发缺陷,引发严重的安全问题.研究表明原子性违反是中断并发缺陷中最突出的一类缺陷模式.目前面向中断驱动型嵌入式软件的原子性违反检测方法都无法同时实现高精度和高可扩展性,且其对真实航天嵌入式软件的有效性尚未得到证实.为了有效提升检测该类缺陷的精度与效率,对82个航天嵌入式软件原子性违反进行实证研究,获得该类缺陷在原子区范围、中断嵌套层数、访问交错模式、共享数据访问方式、访问粒度等5个方面的表现特征.并在此基础上,提出一个精确、高效的原子性违反静态检测方法intAtom-S.首先,基于一个由数值不变式参数化的细粒度内存访问模型,引入基于规则的方法剔除标志变量访问,并采用抽象解释进行精确的共享数据分析,该分析能将共享数据访问粒度精确至数组元素,并可识别共享的内存映射I/O地址.然后,使用轻量级数据流分析技术匹配符合缺陷访问交错模式的所有并发三次访问序,作为潜在的原子性违反缺陷候选.最后,采用基于路径条件的约束求解对缺陷候选中的串行访问对和并发三次访问序进行路径可行性分析,逐步消除误报,得到最终的原子性违反结果.在基准测试集和8个真实航天嵌入式软件上的实验表明,与目前最先进的方法相比,intAtom-S误报率降低了72％,检测效率提高了3倍.此外,该方法能够快速完成对真实航天嵌入式软件的分析,平均误报率仅为8.9％,并发现了23个已被开发人员确认的缺陷.

    航天嵌入式软件中断并发缺陷缺陷特征原子性违反静态分析

      原文链接:
    • NETL
    • NSTL
    • 维普
    • 万方数据

    智能合约Gas优化综述

    宋书玮倪孝泽陈厅
    311-325页
    查看更多>>摘要：区块链2.0最显著的特征是增加了对智能合约的支持,这使得区块链拥有了运行各种应用程序的能力.智能合约是一种根据预先定义的代码逻辑自动运行的计算机软件.区别于传统软件,区块链技术赋予了智能合约不依赖可信中心机构而在相互不信任的节点上正确执行的能力,使其在数字支付、共享经济等领域被广泛地应用.为了防止滥用智能合约导致计算资源被浪费,以太坊等区块链向部署和执行智能合约这2种活动收取Gas(燃料)费用.智能合约消耗的计算资源是决定费用高低的因素.具有低效代码的智能合约浪费资源且易受攻击,此类智能合约的开发者和用户将承担不必要的费用.因此,优化智能合约以节省资源已经成为开发者和研究者重点关注的问题.首先详细分析了智能合约Gas优化所面临的主要挑战;然后回顾和总结了近年来提出的各种优化技术;最后展望了该研究方向的未来工作,旨在为智能合约的开发者和研究人员提供参考和借鉴.

    区块链智能合约Gas优化代码效率软件分析

      原文链接:
    • NETL
    • NSTL
    • 维普
    • 万方数据

    基于控制流和数据流分析的内存拷贝类函数识别技术

    尹小康芦斌蔡瑞杰朱肖雅...
    326-340页
    查看更多>>摘要：内存错误漏洞仍是当前网络攻击中造成危害最严重的漏洞之一.内存错误漏洞的产生往往与对内存拷贝类函数的误用有关.目前针对内存拷贝类函数的识别主要借助于符号表和代码特征模式匹配,具有较高的误报率和漏报率,并且适用性较差.提出了一种内存拷贝类函数识别技术CPYFinder(copy function finder).该技术在内存拷贝类函数控制流特征的基础上,将二进制代码转换为中间语言表示VEX IR(intermediate representation)进行数据流的构建和分析,根据内存拷贝类函数在数据流上的特征进行识别.该技术能够在较低的运行时间下对多种指令集架构(x86,ARM,MIPS,PowerPC)的二进制程序中的内存拷贝类函数进行识别.实验结果表明,相比于最新的工作BootStomp和SaTC,CPYFinder在对内存拷贝类函数识别上具有更好的表现,在精准率和召回率上得到更好的平衡,并且运行时间与SaTC几乎相等,仅相当于BootStomp耗时的19％.此外,CPYFinder在漏洞函数识别上也具有更好的表现.

    静态分析数据流分析中间表示内存拷贝函数函数识别

      原文链接:
    • NETL
    • NSTL
    • 维普
    • 万方数据

    支持多密文等值测试的无线体域网聚合签密方案

    杨小东周航任宁宁袁森...
    341-350页
    查看更多>>摘要：无线体域网(wireless body area network,WBAN)技术拥有低时延和高灵活性的特点,在医疗保健、病情监控和紧急救护等领域拥有广阔的应用前景.针对目前WBAN密码方案中存在的证书管理开销过大、不支持多用户检索与多密文等值测试等问题,提出了一种支持多密文等值测试的WBAN聚合签密方案.采用基于身份的签密体制,消除了传统公钥密码方案中的证书管理问题,保证了医疗数据的机密性与可认证性.利用聚合签密技术,降低了多用户环境下对医疗密文进行验证的计算开销.引入多密文等值测试技术,实现了多数据用户同时对多医疗密文的安全检索,提高了多用户环境下密文检索的效率.在随机预言模型下,基于计算性Diffie-Hellman困难问题证明了该方案在适应性选择密文攻击下的单向性.与同类方案相比较,该方案支持更多的安全属性,并具有较低的计算开销.

    无线体域网多用户环境多密文等值测试聚合签密基于身份的签密

      原文链接:
    • NETL
    • NSTL
    • 维普
    • 万方数据

    支持一般电路的高效安全基于属性签名

    黄振杰林志伟
    351-361页
    查看更多>>摘要：基于属性签名(attribute-based signature,ABS)是一种重要的密码原语,具有广泛的应用背景,得到众多学者的关注,是密码学的研究热点.为了提高基于属性签名的安全性、表达力和效率,使用多线性映射作为工具,提出一个支持一般电路的具有完善隐私性的基于属性签名方案.引入节点权重概念并采用"从上到下"递归,显著减少生成签名的计算开销;利用左右孩子节点的对称性,缩短门节点的密钥长度.所提出的方案将不可伪造性从"选定消息且选定属性攻击下存在不可伪造"提升到更强的"自适应选择消息但选定属性攻击下存在不可伪造";将访问结构从特殊电路拓展到一般电路,可以支持任意访问结构,达到任意的访问控制粒度;在保持签名仅为1个群元素的前提下,显著缩短主公钥、主私钥和签名钥的大小和显著降低签名密钥生成、签名生成和验证的计算开销.分析表明:所提出的方案在性能和效率方面均有明显优势,是一个实用的方案.

    基于属性签名一般电路多线性映射完善隐私性密钥策略

      原文链接:
    • NETL
    • NSTL
    • 维普
    • 万方数据