Abstract: Software development for complex systems requires
efficient and automatic tools that can be used to verify the
satisfiability of some critical properties such as security ones. With
the emergence of Aspect-Oriented Programming (AOP), considerable
work has been done in order to better modularize the separation of
concerns in the software design and implementation. The goal is to
prevent the cross-cutting concerns to be scattered across the multiple
modules of the program and tangled with other modules. One of the
key challenges in the aspect-oriented programs is to be sure that all
the pieces put together at the weaving time ensure the satisfiability
of the overall system requirements. Our paper focuses on this problem and proposes a formal property
verification approach for a given property from the woven program.
The approach is based on the control flow graph (CFG) of the
woven program, and the use of a satisfiability modulo theories (SMT)
solver to check whether each property (represented par one aspect)
is satisfied or not once the weaving is done.
Abstract: Control Flow Integrity (CFI) is one of the most
promising technique to defend Code-Reuse Attacks (CRAs).
Traditional CFI Systems and recent Context-Sensitive CFI use coarse
control flow graphs (CFGs) to analyze whether the control flow
hijack occurs, left vast space for attackers at indirect call-sites. Coarse
CFGs make it difficult to decide which target to execute at indirect
control-flow transfers, and weaken the existing CFI systems actually.
It is an unsolved problem to extract CFGs precisely and perfectly
from binaries now. In this paper, we present an algorithm to get a
more precise CFG from binaries. Parameters are analyzed at indirect
call-sites and functions firstly. By comparing counts of parameters
prepared before call-sites and consumed by functions, targets of
indirect calls are reduced. Then the control flow would be more
constrained at indirect call-sites in runtime. Combined with CCFI,
we implement our policy. Experimental results on some popular
programs show that our approach is efficient. Further analysis show
that it can mitigate COOP and other advanced attacks.
Abstract: Control flow graphs are a well-known representation of
the sequential control flow structure of programs with a multitude
of applications. Not only single functions but also sets of functions
or complete programs can be modeled by control flow graphs. In
this case the size of the graphs can grow considerably and thus
makes it difficult for software engineers to analyze the control flow.
Graph reductions are helpful in this situation. In this paper we define
reductions to subsets of nodes. Since executions of programs are
represented by paths through the control flow graphs, paths should
be preserved. Furthermore, the composition of reductions makes a
stepwise analysis approach possible.
Abstract: The ever-growing usage of aspect-oriented
development methodology in the field of software engineering
requires tool support for both research environments and industry. So
far, tool support for many activities in aspect-oriented software
development has been proposed, to automate and facilitate their
development. For instance, the AJaTS provides a transformation
system to support aspect-oriented development and refactoring. In
particular, it is well established that the abstract interpretation of
programs, in any paradigm, pursued in static analysis is best served
by a high-level programs representation, such as Control Flow Graph
(CFG). This is why such analysis can more easily locate common
programmatic idioms for which helpful transformation are already
known as well as, association between the input program and
intermediate representation can be more closely maintained.
However, although the current researches define the good concepts
and foundations, to some extent, for control flow analysis of aspectoriented
programs but they do not provide a concrete tool that can
solely construct the CFG of these programs. Furthermore, most of
these works focus on addressing the other issues regarding Aspect-
Oriented Software Development (AOSD) such as testing or data flow
analysis rather than CFG itself. Therefore, this study is dedicated to
build an aspect-oriented control flow graph construction tool called
AJcFgraph Builder. The given tool can be applied in many software
engineering tasks in the context of AOSD such as, software testing,
software metrics, and so forth.