共查询到19条相似文献,搜索用时 265 毫秒
1.
可执行可信软件安全性分析技术研究 总被引:1,自引:0,他引:1
为了保证基于可信架构的可信软件的安全性,给出了可信软件安全性分析的总体架构及其工作原理,提出了一个静态分析技术与动态测试技术相结合的有效机制,实现了静态分析和动态跟踪的交互协作,提高了安全分析的效率.设计了一种可执行代码中间表示的方法,给出了建立程序存储空间抽象模型和程序抽象运行时刻环境的方法.详细地讨论了程序的控制流和数据流分析技术,并给出了求解算法.最后,概述了程序动态测试系统. 相似文献
2.
3.
4.
5.
6.
通过在通用单调数据流框架基础上使用基于抽象解释的变量值范围传播技术,本文提出了一种自动获取循环最大迭代次数和不可行路径的方法。该方法有利于精确计算实时程序最差情况下的执行时间(WCET)。 相似文献
7.
对于高性能并行计算机而言,如何由给出的计算、数据划分信息及精确数组数据流分析信息自动生成并行化代码是实现串行程序并行化的一个重要问题。根据Saman P.Amarasinghe和Lam的定理,实现了一种并行化识别工具中MPI(Message Passing Interface)并行化代码自动生成技术的算法,并对该算法的性能进行分析。 相似文献
8.
JUTA: 一个Java自动化单元测试工具 总被引:2,自引:0,他引:2
描述了一个Java自动化的单元测试工具JUTA.JUTA首先调用工具Soot解析单个Java方法的源码,并将源码解析成一个控制流图.在此基础上,采用符号执行的方法分析控制流图上的路径.工具能够自动地产生满足覆盖率标准的程序的测试用例.这种方法产生的所有测试用例都是可执行的,并且一般来说具有较小的测试用例数.如果用户能够合理地给出描述程序错误的断言,框架JUTA能够自动地检查源码中部分特定类型的错误.实验结果表明工具对Java单元代码的动态测试和静态测试均能在可接受的时间内给出有效的结果. 相似文献
9.
在安全关键领域中,如何保证软件的安全性已经成为了一个广受关注的重要课题。静态程序分析是一类十分有效的程序自动化验证方法。基于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出。可配置程序分析(Configurable Program Analysis,CPA)是一种通用静态分析方法形式化体系,旨在用一种形式化体系对静态分析的分析阶段进行建模。使用CPA对基于抽象解释的静态分析进行建模,给出如何使用CPA形式化体系描述基于抽象解释的静态分析,给出了从待分析程序到CPA形式化体系的转换规则;提供了一种在安全关键性领域中的软件正确性自动验证方法,为基于抽象解释的静态分析工具的实现提供了一种可行方案。 相似文献
10.
本文给出了对自动化可移植代码生成技术的分类,并对有关这些技术的工作进行了综述。可移植代码生成的研究方法共分三类:解释代码生成,模式匹配代码生成以及表驱动代码生成。解释代码生成方法是先为虚拟机生成代码,然后再把该代码扩展成实际目标代码。模式匹配代码生成方法是把机器描述和代码生成算法分离。表驱动代码生成方法是利用形式化的机器描述和代码生成程序的生成程序,自动构造代码生成程序。本文对这些技术进行分析,并对各种自动代码生成算法进行评述。 相似文献
11.
一种基于抽象解释和通用单调数据流框架的值范围分析方法 总被引:2,自引:0,他引:2
安全而又精确的值范围分析对编译器优化至关重要.系统地提出了一个基于抽象解释和通用单调数据流框架的值范围分析框架,包括精确的定叉、分析和完整的正确性证明.与一般的值范围分析方法不同,该框架不仅包括抽象解释,还包括与之对应的具体解释,以及相应的正确性证明. 相似文献
12.
We derive a security flow control algorithm for message-based, modular systems and prove the algorithm correct. The development is noteworthy because it is completely rigorous: the flow control algorithm is derived as an abstract interpretation of the denotational semantics of the programming language for the modular system, and the correctness proof is a proof by logical relations of the congruence between the denotational semantics and its abstract interpretation. Effectiveness is also addressed: we give conditions under which an abstract interpretation can be computed as a traditional iterative data flow analysis, and we prove that our security flow control algorithm satisfies the conditions. We also show that symbolic expressions (that is, data flow values that contain unknowns) can be used in a convergent, iterative analysis. An important consequence of the latter result is that the security flow control algorithm can analyse individual modules in a system for well formedness and later can link the analyses to obtain an analysis of the entire system. 相似文献
13.
Cinzia Bernardeschi Marco Di Natale Gianluca Dini Maurizio Palmieri 《Journal in Computer Virology》2018,14(4):269-289
This paper presents an approach for enhancing the design phase of AUTOSAR models when security annotations are required. The approach is based on information flow analysis and abstract interpretation. The analysis evaluates the correctness of the model by assessing if the flow of data is secure with respect to causal data dependencies within the model. To find these dependencies an exhaustive search through the model would be required. Abstract interpretation is used as a trade-off between the precision and complexity of the analysis. The approach also provides annotated models without oversizing the set of annotations. 相似文献
14.
15.
单变量区间线性不等式抽象域 总被引:4,自引:0,他引:4
程序变量的值范围信息对于编译器优化、程序分析与验证等应用至关重要.抽象解释理论提供了一种通用框架为程序变量计算近似的但是可靠的值范围.然而该框架下已有的数值抽象域在表达非凸性质方面存在一定的局限性,影响了值范围分析的精度.文中基于抽象解释理论,提出一个新的数值抽象域——单变量区间线性不等式抽象域.其主要思想是使用单变量区间线性不等式约束作为域元素的约束表示方法.该抽象域的表达能力强于经典的区间抽象域,并允许表达某类非凸、非连通性质.同时,其域操作存在高效的实现算法.该抽象域具有很强的可扩展性,能够应用在实际大规模的程序分析中. 相似文献
16.
Florian Martin 《International Journal on Software Tools for Technology Transfer (STTT)》1998,2(1):46-67
The program analyzer generator PAG described in this paper attempts to offer the best of both worlds, specification languages
based on the clean theory of abstract interpretation and efficient implementation methods from the theory of data flow analysis.
PAG has a high level functional input language to specify data flow analyses. It offers the generation of complex data structures
and is therefore not limited to bit vector problems. PAG generated interprocedural analyzers can be easily integrated into
existing compilers.
PAG has successfully been used in the ESPRIT project COMPARE to generate several analyzers (including alias analysis and
constant propagation) for industrial quality ANSI-C and Fortran90 compilers, and is now marketed by the spin-off company AbsInt.A
simplified version of PAG can be interactively tested over the Web. 相似文献
17.
18.
Flemming Nielson 《Acta Informatica》1982,18(3):265-287
Summary It is shown how to express data flow analysis in a denotational framework by means of abstract interpretation. A continuation style formulation naturally leads to the MOP (Meet Over all Paths) solution, whereas a direct style formulation leads to the MFP (Maximal Fixed Point) solution. 相似文献