Commit b67dd64b authored by Rick Smetsers's avatar Rick Smetsers
Browse files

Modified Joshua's addition to the introduction a bit

parent b987aea1
......@@ -63,7 +63,9 @@ Software systems are becoming increasingly complex.
\emph{Model learning} is quickly becoming a popular technique for reverse engineering such systems.
Instead of viewing a system via its internal structure, model learning algorithms construct a formal model from observations of a system's behaviour.
One prominent approach for model learning is described in a seminal paper by \citet{angluin1987learning}.
\medskip
\noindent One prominent approach for model learning is described in a seminal paper by \citet{angluin1987learning}.
In this work, she proved that one can efficiently learn a model that describes the behaviour of a system if a so-called \emph{Minimally Adequate Teacher} is available.
This teacher is assumed to answer two types of questions about the (to the learner unknown) \emph{target}:
\begin{itemize}
......@@ -80,8 +82,10 @@ Membership queries, on the one hand, are implemented simply by interacting with
Equivalence queries, on the other hand, require a more elaborate approach, as there is no trivial way of implementing them.
Therefore, an ongoing challenge, and the topic of this paper, is to efficiently obtain counterexamples.
\medskip
% Current techniques for implementing equivalence queries
Several techniques for obtaining counterexamples have been proposed.
\noindent Several techniques for obtaining counterexamples have been proposed.
The most widely studied approach for this purpose is \emph{conformance testing} \citep{Dorofeeva2010}.
In the context of learning, the goal of conformance testing is to establish an equivalence relation between the current hypothesis and the target.
This is done by posing a set of so-called \emph{test queries} to the system.
......@@ -101,8 +105,10 @@ Second, it is known that testing becomes exponentially more expensive for higher
Therefore, the learner might incorrectly assume that its hypothesis is correct.
This motivates the search for alternative techniques for implementing equivalence queries.
\medskip
% Fuzzing as a way of implementing equivalence queries
The field of \emph{mutation-based fuzzing} provides opportunities here.
\noindent The field of \emph{mutation-based fuzzing} provides opportunities here.
In essence, \emph{fuzzers} are programs that apply a test (i.e.\ input sequence) to a target program, and then iteratively modify this sequence to monitor whether or not something interesting happens (e.g.\ crash, different output, increased code coverage \ldots).
Fuzzers are mostly used for security purposes, as a crash could uncover an exploitable buffer overflow, for example.
%In general, two classes of fuzzers exist.
......@@ -112,6 +118,7 @@ Fuzzers are mostly used for security purposes, as a crash could uncover an explo
%Therefore, these fuzzers offer no solution to the exponential blow-up of conformance testing.
%On the other hand, more sophisticated \emph{generation-based} fuzzers modify the test query based on some specification of the target program.
%This is effective in terms of the number interesting test queries generated, but unfortunately also requires one to write this potentially complex specification.
Recently, good results have been achieved by combining mutation-based fuzzing with a genetic (evolutionary) algorithm.
This requires a fitness function to evaluate the performance of newly generated test query, i.e.\ a measurement of `how interesting' it is.
In our case, this fitness function is based on what code is executed for a certain test query.
......@@ -120,22 +127,25 @@ Hence, tests are mutated to see if the coverage of the program is increased.
Iterating this process creates an evolutionary approach which proves to be very effective for various applications \citep{afl-website}.
\subsection{RERS Challenge 2016}
In this paper we report on our experiments in which we apply above techniques to the RERS challenge 2016.
The challenge consists of two parts: 1) problems for which we have to prove or disprove certain properties and 2) problems for which we have to find the reachable error states.
The problems are provided as source code (either C or Java) which are derived from some FSM.
To describe our approach briefly, we used a state of the art learning algorithm with a decent conformance testing algorithm.
Furthermore we used a fuzzer to generate potentially interesting traces.
For part (1) of the challenge the fuzzer did not find any counter examples.
For part (2) it did, which resulted in more error states being reached.
Due to time constraints we isolated learning and fuzzing.
We plan to experiment with integrating fuzzing in the learning loop.
\subsubsection*{RERS Challenge 2016}
In this report we describe our experiments in which we apply the aforementioned techniques to the \emph{Rigorous Examination of Reactive Systems} (RERS) challenge 2016.
The RERS challenge consists of two parts:
\begin{enumerate}
\item \emph{problems} (i.e. reactive software) for which one has to prove or disprove certain logical properties, and
\item problems for which one has to find the reachable error states.
\end{enumerate}
\noindent In our approach, we have used a state of the art learning algorithm (\emph{learner}) in combination with a conformance testing algorithm (\emph{tester}) to learn models for the RERS 2016 problems.
In addition, we have used a mutation-based fuzzing tool (\emph{fuzzer}) to generate potentially interesting traces independently of the learner and the tester.
We have used these traces as a verification for the learned models and found that
\begin{itemize}
\item For part (1) of the challenge the fuzzer did not find any additional counterexamples for the learner, compared to those found by the tester.
\item For part (2) of the challenge the fuzzer discovered more reachable error states than the learner and tester, albeit the learner and tester found some that were not discovered by the fuzzer.
\end{itemize}
\noindent Our experiments lead us to believe that in some applications, fuzzing is a viable technique for finding \emph{additional} counterexamples for a learning setup.
In this report, in addition to describing our experimental setup for RERS in detail, we therefore describe possible ways of combining learning and fuzzing.
%\subsubsection*{Related work}
%\citet{Duchene2012} have used a combination of model learning and evolutionary mutation-based fuzzing to detect web injection vulnerabilities.
......@@ -165,7 +175,7 @@ We plan to experiment with integrating fuzzing in the learning loop.
%A major limitation of this approach is that the quality of the learned model heavily relies on the diversity of the traces that are (passively) being observed.
\section{Preliminaries}
In this section, we describe preliminaries on finite state machines, active learning, conformance testing, and fuzzing.
In this section, we describe preliminaries on finite state machines, model learning, conformance testing, and fuzzing.
%Where possible, we will illustrate these concepts by means of their application to the vending machine implementation shown in \autoref{fig:fsm}.
%\begin{figure}%
......@@ -248,8 +258,8 @@ A \emph{discriminator} for a pair of states $q, q'$ is an input sequence $x \in
The behaviour of a FSM $M$ is defined by a \emph{characterization function} $A_M : I^{\ast} \to O^{\ast}$ with $A_M(x) = \lambda(q_M, x)$ for $x \in I^{\ast}$.
FSMs $M$ and $M'$ are \emph{equivalent} if $A_M(x) = A_{M'}(x)$ for $x \in I^{\ast}$.
\subsection{Active learning} \label{sec:learning}
The goal of active learning algorithms is to learn a FSM $H = (I, O, Q_H, q_H, \delta_H, \lambda_H)$ for a system whose behaviour can be characterized by a (unknown) FSM $M = (I, O, Q_M, q_M, \delta_M, \lambda_M)$, given the set of inputs $I$ and access to the characterization function $A_M$ of $M$.
\subsection{Model learning} \label{sec:learning}
The goal of so-called active model learning algorithms is to learn a FSM $H = (I, O, Q_H, q_H, \delta_H, \lambda_H)$ for a system whose behaviour can be characterized by a (unknown) FSM $M = (I, O, Q_M, q_M, \delta_M, \lambda_M)$, given the set of inputs $I$ and access to the characterization function $A_M$ of $M$.
%Angluin's original $L^{\ast}$ algorithm \cite{angluin1987learning} incrementally constructs and refines a so-called \emph{observation table}.
%The rows and columns of an observation table are labelled by prefixes and suffixes of membership queries respectively, and the cells are filled with the last output in response to this membership query.
......@@ -557,7 +567,7 @@ Second, we describe the systems presented in the \emph{Rigorous Examination of R
We conclude this section by presenting the results of these experiments.
\subsection{Experimental setup}
For our experiments, we have combined AFL with LearnLib, an open-source Java library for active learning \citep{merten2011learnlib}\footnote{Code available at \url{https://github.com/praseodym/learning-fuzzing}.}.
For our experiments, we have combined AFL with LearnLib, an open-source Java library for active model learning \citep{merten2011learnlib}\footnote{Code available at \url{https://github.com/praseodym/learning-fuzzing}.}.
To answer equivalence queries using AFL we have implemented a new equivalence oracle, \lstinline!AFLEQOracle!.
This oracle iteratively loads a test that AFL marks as interesting, and parses them as a sequence of inputs.
As AFL does not use a fixed set of inputs, any inputs that are not known by the learner are skipped.
......@@ -843,7 +853,7 @@ First, as noted in \autoref{sec:results}, combining fuzzing with conformance tes
Currently, this approach requires a lot of time.
Therefore, it would be interesting to combine the approaches in a way that harnesses the strengths of both methods (i.e.\ a `small', yet complete test set with maximum coverage).
Second, it is possible to use \emph{passive learning} techniques (i.e. learning from observations) on test cases generated by a mutation-based fuzzer.
It would be interesting to compare this to the active learning approaches discussed in this paper with regard to learning time and the quality of the learning model in terms of overall correctness.
It would be interesting to compare this to the active model learning approaches discussed in this paper with regard to learning time and the quality of the learning model in terms of overall correctness.
Third, it would be interesting to relate transitions in a learned finite state machine to the code that is executed during these transitions.
This could be combined with tainting to show how input values influence behaviour.
Finally, the AFL-LLVM compiler could be adapted to work on LLVM IR \citep{LLVMLangRef} (generally encoded as LLVM Bitcode \cite{LLVMBitCodeFormat}), which would allow it to instrument existing binaries if they can be disassembled to LLVM IR.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment