environment.tex

% !TEX root = main.tex

\section{Interaction with the environment}
\label{se:environment-thirdparty}

\revedit{As most programs are not self-contained, a symbolic engine has to take into account their frequent interactions with the surrounding software stack. A typical example is data flows that take place through features of the underlying operating system (e.g., file system, environment variables, network). Functions controlled by the system environment are often referred to as {\em external}. Modern applications pose further challenges when they interact with the user via other components (e.g., Swing, Android), or invoke special features of their execution runtimes. Missing symbolic data flows through these software elements might indeed affect the meaningfulness of the analysis.}
 
\revedit{\myparagraph{System Environment}}
% symbolic analysis \revedit
A body of early works (e.g., {\sc DART}~\cite{DART-PLDI05},  {\sc CUTE}~\cite{CUTE-FSE05}, and {\sc EXE}~\cite{EXE-CCS06}) include the \revedit{system} environment in the analysis by actually executing external calls using concrete arguments for them. This indeed limits the behaviors they can explore compared to a fully symbolic strategy, which on the other hand might be unfeasible. 
%
In an online executor this choice may also result in having external calls from distinct paths of execution interfere with each other. As there is no mechanism for tracking the side effects of each external call, there is potentially a risk of state inconsistency, e.g., an execution path may read from a file while at the same time another execution path is trying to delete it.

%Another way to tackle the problem is to create an abstract model that captures these interactions 
A way to overcome this problem is to create abstract models that capture these interactions. For instance, in {\sc KLEE}~\cite{KLEE-OSDI08} symbolic files are supported through a basic {\em symbolic file system} for each execution state, consisting of a directory with $n$ symbolic files whose number and sizes are specified by the user. An operation on a symbolic file results in forking $n+1$ state branches: one for each possible file, plus an optional one to capture unexpected errors in the operation. As the number of functions in a standard library is typically large and writing models for them is expensive and error-prone~\cite{Ball06}, models are generally implemented at system call-level rather than library level. This enables the symbolic exploration of the libraries as well.

% {\sc CLOUD9} further extends support to many other POSIX libraries, allowing users to also control advanced conditions in the testing environment. For instance, it can simulate reordering, delays, and packet dropping caused by a fragmented data stream over a network.
{\sc AEG}~\cite{AEG-NDSS11} models most of the system environment that could be used by an attacker as input source, including the file system, network sockets, and environment variables. Additionally, more than 70 library and system calls are emulated, including thread- and process-related system calls, and common formatting functions to capture potential buffer overflows. Symbolic files are handled as in {\sc KLEE}~\cite{KLEE-OSDI08}, while symbolic sockets are dealt with in a similar manner, with packets and their payloads being processed as in symbolic files and their contents. {\sc CLOUD9}~\cite{CLOUD9-EUROSYS11} supports additional POSIX libraries, and allows users to control advanced conditions in the testing environment. For instance, it can simulate reordering, delays, and packet dropping caused by a fragmented network data stream.

{\sc \stwoe}~\cite{CKC-TOCS12} remarks that models, other than expensive to write, rarely achieve full accuracy, and may quickly become stale if the modeled system changes. 
%\sc \stwoe}~\cite{CKC-TOCS12} remarks that models, other than expensive to write, rarely achieve full accuracy, and may quickly become stale if the modeled system changes. Hence, it would be preferable to let analyzed programs interact with the real environment while exploring multiple paths. In their \stwoe\ platform, the authors rely on virtualization to perform the desired analysis on the real software stack, preventing side effects from propagating across independent execution paths.
It would thus be preferable to let analyzed programs interact with the real environment while exploring multiple paths. However, this must be done without incurring in environment interferences or state inconsistencies. To achieve this goal, \stwoe\ resorts to virtualization to prevent propagation of side effects across independent execution paths when interacting with the real environment. QEMU~\cite{QEMU-ATC05} is used to emulate the full software stack: instructions are transparently translated into micro operations run by the native host, while an x86-to-LLVM lifter is used to perform symbolic execution of the instructions sequence in {\sc KLEE}~\cite{KLEE-OSDI08}. This allows {\sc \stwoe} to properly evaluate any side-effects due to the environment. Notice that whenever a symbolic branch condition is evaluated, the execution engine forks a parallel instance of the emulator to explore the alternative path. Selective symbolic execution (Section~\ref{ss:concrete-concolic-symbolic}) is used to limit the scope of symbolic exploration across the software stack, partially mitigating the overhead of emulating a full stack \revedit{(e.g., user code, libraries, drivers)} that can significantly limit the scalability of the overall solution.

%\mytempedit{Hence, it would be preferable to let analyzed programs interact with the real environment while exploring multiple paths. However, this must be done without incurring in environment interferences or state inconsistencies. To achieve this goal, the authors of the \stwoe\ platform rely on virtualization to perform the desired analysis on the real software stack, preventing side effects from propagating across independent execution paths. \stwoe\ exploits QEMU~\cite{QEMU-ATC05} for running the full software stack, translating guest instructions into micro-operations that can easily be run on top of the native host. Additionally, a x86-to-LLVM backend allows \stwoe\ to symbolically analyze any instruction using KLEE. By emulating the full software stack -- from the application to the operating system -- it is possible to properly evaluate any side-effects due to the environment. Whenever a symbolic branch condition is evaluated by \stwoe, a {\tt fork} operation is performed by the engine and a parallel instance of the emulator is spawned to explore the alternative path. Unfortunately, analyzing a whole-system in this manner hardly scales in practice due to the path explosion problem. For this reason, \stwoe\ has been designed for performing symbolic execution of a program without the burden of exploring any uninteresting paths that could be generated due to library and kernel code. This is achieved through the use of {\em selective symbolic execution}: this technique allows \stwoe\ to interleave symbolic (multi-path) exploration of the program code with concrete (single-path) execution of the external code. To avoid that any interesting path in the program code could be missed due to the concretization done when executing external code, \stwoe\ defines different consistency models that in turn guarantee different trade-offs with respect to the analysis correctness (see Section~\ref{ss:concrete-concolic-symbolic} for more details). For instance, \stwoe\ is able to run concretely some external code and later detect whether the concretization is impacting the symbolic exploration of the program code. Intuitively, in this case, a new concrete execution of the external code can be started, choosing different concrete input arguments in a way that can allow the engine to later explore the skipped paths. Although this approach makes it possible to properly handle most of the side effects due to the environment, the overhead of emulating the full stack can be significantly high, limiting the scalability of the overall solution.

% that possibly will allow the engine to explore the previously missed path.
%Intuitively, whenever a call to a library or kernel function is done by the program code, a single concrete execution is actually performed by the engine. Although a single concrete input instance is chosen, the engine tracks the path constraints during the concrete execution of the external code. This makes it possible to precisely characterize the input family that the chosen input instance is representative of. When returning from the external code, these path constraints are added to 


{\sc DART}'s approach~\cite{DART-PLDI05} is different, as the goal is to enable automated unit testing. DART deems as foreign interfaces all the external variables and functions referenced in a C program along with the arguments for a top-level function.
%External interfaces are identified by parsing the source code, and a random test driver is generated accordingly.
External functions are simulated by nondeterministically returning any value of their specified return type. To allow the symbolic exploration of library functions that do not depend on the environment, the user can adjust the boundary between external and non-external functions to tune the scope of the symbolic analysis.
%Library functions are normally not considered external functions as they are controlled by the program, but in practice the user can adjust the boundary between library and external functions to simulate the desired effects.

% symbolically analyzed
\revedit{\myparagraph{Application Environment}}
\revedit{We now discuss possible solutions for dealing with software elements that carry out control and data flows on the behalf of the program under analysis. Instances of this problem arise for instance in frameworks like Swing and Android, which embody abstract designs to invoke application code (e.g., via callbacks) during user interaction~\cite{JQF-ICSE16}. Symbolic values flow outside the boundaries of the analysis also for applications running in managed runtimes, e.g., when calling native Java methods or unmanaged code in .NET~\cite{AOH-TACAS07}. Such features complicate the implementation of an engine: for instance, native methods and reflection in Java depend on the internals of the underlying JVM~\cite{Anand12}. Closed-source components might represent another instance of this problem.}

%Calls to native Java methods, unmanaged code in .NET, or closed-source components are other typical scenarios where symbolic values may flow outside the boundaries of the code under analysis~\cite{AOH-TACAS07}. Notice also that native methods and reflection features in Java depend on the internals of the underlying Java runtime~\cite{Anand12}.}
%that carry out significant control and data flows on the behalf of the application.

%Calls to native Java methods, unmanaged code in .NET, or closed-source components are typical instances of a scenario where symbolic values may flow outside the boundaries of the code being analyzed~\cite{AOH-TACAS07}. For instance, frameworks such as Swing and Android embody abstract designs to invoke application code (e.g., via callbacks) \revedit{during user interaction} that an engine must account for~\cite{JQF-ICSE16}. Furthermore, native methods and reflection features in Java  depend on the internals of the underlying Java virtual machine~\cite{Anand12}.

%For instance, an engine must account for the fact that native methods and reflection features in Java depend on the internals of the underlying Java virtual machine~\cite{Anand12}. Moreover, frameworks like Java Swing or the Android platform have important control and data flows occurring within the framework, such as callbacks for events, that would be missed by a symbolic execution of the application code only~\cite{JQF-ICSE16}.

%Similar challenges are faced when in the analysis of real-world software symbolic values flow outside the boundaries of the code being symbolically executed. Common instances of this problem are calls to, e.g., native methods in Java, unmanaged code in the .NET framework, and third-party closed-source libraries.

% we should cite EXE-TECH06 but we get the same identifier :-(
%{\sc EXE}~\cite{EXE-CCS06} instead devises a trial-and-error strategy so that calls with symbolic arguments to external library functions are logged, and the user has to manually intervene to instrument the external code and restart the exploration. This methodology aims at ensuring more complete constraint generation compared to concretization, but may require repeated interaction with the user and not scale for large functions.

%possibly resulting in an incomplete exploration and in turn failing to generate test inputs for feasible program paths
Similarly as in \revedit{system} environment modeling, early works such as {\sc DART}~\cite{DART-PLDI05} and {\sc CUTE}~\cite{CUTE-FSE05} deal with calls to \revedit{other software} components by executing them with concrete arguments. This may result in an incomplete exploration, failing to generate test inputs for feasible program paths. On the other hand, a symbolic execution of their code is unlikely to succeed for a number of reasons: for instance, the implementation of externally simple behaviors is often complex as it has to allow for extensibility and maintainability, or may contain details irrelevant to the exploration, such as how to display a button that triggers a callback~\cite{JQF-ICSE16}.
%
%such components often devise complex implementations of externally simple behaviors in order to allow for extensibility and maintainability, or may contain details irrelevant to the exploration such as the graphical representation of a feature.
%
One solution would be to mimic external components with simpler and more abstract models. However, writing component models manually -- which can be a daunting task per se -- might be hard due to the unavailability of the source code, and applications using unsupported models would remain out of reach.

%as in general models cannot be reused across components, applications that use unsupported ones remain out of reach. 

% that are heavily used
Some works (e.g., \cite{AOH-TACAS07,XXT-ICSE11}) explore techniques to pinpoint which entities from a component may hold symbolic values in a symbolic exploration, and thus require human intervention (e.g., writing a model) for their analysis. A different line of research has instead attempted to generate models automatically, which may be the only viable option for closed-source components. \cite{CT-SEN14,VTV-SEN15} employ program slicing to extract the code that manipulates a given set of fields relevant for the analysis, and build abstract models from it. \cite{JQF-ICSE16} takes a step further by using program synthesis to produce models for Java frameworks. Such models provide equivalent instantiations of design patterns that are heavily used in many frameworks: this helps symbolic executors discover control flow -- such as callbacks to user code through an observer pattern -- that would otherwise be missed. An advantage of using program synthesis is that it can generate more concise models than slicing, as it abstracts away the details and entanglements of how a program is written by capturing its functional behavior.
%
%Some\mynote{[D] work in progress}  works (e.g., \cite{AOH-TACAS07,XXT-ICSE11}) have explored techniques to pinpoint which entities in a component a symbolic exploration would need a model for. A different line of research has instead attempted to generate models automatically, which can also be valuable for closed-source components. For instance, program slicing has been used to generate models for Android~\cite{VTV-SEN15} and Swing~\cite{CT-SEN14}. \cite{JQF-ICSE16} takes a step further by using program synthesis to produce models for Java frameworks that make use of design patterns, which are heavily \mynote{I: non chiaro, a che si riferisce often also to carry out ...? Forse va rifrasata o tolta?} used in many components, often also to carry out control and data flows. An advantage of program synthesis is that it can generate more concise models than slicing, as it is not constrained by the structure of the implementation. %We further elaborate on program synthesis at the end of Section~\ref{ss:program-analysis}.
%
%Researchers have thus focused on techniques that either pinpoint the sole functions from a component that require a symbolic exploration (e.g., \cite{AOH-TACAS07,XXT-ICSE11}) and thus a model, or attempt to generate models automatically, which can be valuable also for closed-source components. In particular, for the latter approach some works have employed program slicing (Section~\ref{ss:program-analysis}) to generate models for Android~\cite{VTV-SEN15} and Swing~\cite{CT-SEN14}. A further step towards generality is taken in~\cite{JQF-ICSE16}, which uses program synthesis to produce models for Java frameworks that make use of design patterns. The work stems from the observation that design patterns are heavily used in many components, often also for carrying out control and data flows within them. Compared to the techniques based on slicing, it can generate more concise models as program synthesis is not constrained by the structure of the implementation. We further elaborate on program synthesis at the end of Section~\ref{ss:program-analysis}.