Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
Edits to section 3.3
  • Loading branch information
joc02012 committed Jun 11, 2016
1 parent 634db80 commit 2381918
Showing 1 changed file with 28 additions and 24 deletions.
52 changes: 28 additions & 24 deletions AADLSecPaper.tex
Expand Up @@ -183,7 +183,7 @@ More current work on the development of a security annex for AADL has been relea

% Add in an image of attack surface graphical representation
\begin{figure}
\includegraphics[width=\textwidth, height=6cm]{./images/attackAnalysisZoom.png}
\centering\includegraphics[height=6cm]{./images/attackAnalysisZoom.png}
\caption{Graphical Example of AADL Security Annex Attack Impact Analysis~\cite{AADLSecAnalysis}}
\label{fig:AADLAttackAnalysis}
\end{figure}
Expand All @@ -192,8 +192,8 @@ More current work on the development of a security annex for AADL has been relea
Due to the ease by which the user community can add and expand upon the existing AADL lexicon, this paper will have to narrow its examination of additional plug-in and tools to those that have more exposure in examples and other reference materials~\cite{Osate2Examples}\cite{UserDaysMay2016}. The rest of this section will examine Resolute, RDALTE, EMV2, BLESS, and security extensions and annexes.

Resolute is a language and tool for developing architectural assurance cases~\cite{AADLResolute}. Through this tool users are able to formulate claims and rules that are used to justify these user-defined claims. Resolute then takes these claims and constructs assurance cases that are then verified and validated for a given architectural model. Using this tool a user is able to reason about the flow of information through a system and the availability of resources under different operating modes~\cite{gacek2014resolute}. This is advantageous because the same mechanism that allows for Resolute to model requirements of a system's architecture from an early phase, can also be tweaked to track basic security requirements of components that make up the architectural base of a design. Coupled with Resolute's verification of these user-defined assurances, it can be easily seen as to why Resolute can be an effective tool for tracking security requirements across architectural abstractions and with some tinkering of the AADL language could even be used to track higher level requirements of the system as a whole. Implementation of this concept has been seen in Ellison et.~al.'s work for the purpose of checking read, write, and execution privileges over a given system model~\cite{ellison2015extending}. %, as shown in Figure~\ref{fig:AADLResoluteExample}.
Future work of this tool is aimed towards allow for exportation of the defined assurance cases to other tools as well~\cite{gacek2014resolute}. Unfortunately there has not been much work toward this goal. When examining the security-based extensions to AADL, Resolute would make an effective method of verification and validation that a produced security model meets all of the required user-defined security assurances. These could range from networking connectivity requirements to dependencies on correctly implemented access control parameters. The disadvantge of this tool, in its current state, is that the assurance checks are relatively simple and there has been little to no documentation on the user-community's efforts to improve the tool for security-centric applications of modeling.

Future work of this tool is aimed towards allow for exportation of the defined assurance cases to other tools as well~\cite{gacek2014resolute}. Unfortunately there has not been much work toward this goal.
%% Add in an image of resolute being used as a security verification tool
%\begin{figure}
% \includegraphics[width=\textwidth]{./images/resoluteExample.png}
Expand All @@ -203,25 +203,28 @@ Resolute is a language and tool for developing architectural assurance cases~\ci

The Requirements Definition and Analysis Language Tool Environment (RDALTE) is a requirements modeling and validation tool for AADL. This tool allows for organizing requirements and assumptions into packages~\cite{RDALOverview}; allowing for users to group dependent requirements into common packages. RDALTE helps to separate concerns between the requirements and the constraints of a system, while also detailing a clear identification between assumptions and requirements. RDALTE would allow for constructive overlap of security requirements with the Resolute tool, while the constraint definition aspect can be used for describing both the component and security constraints that an embedded systems model must maintain.

The Error-Model Annex is purposed with tracking errors and their propagation throughout a system. The annex can also be used to describe component error behavior as transitions between different states, where transitions are triggered by error events and incoming propagations of error from other parts of the system design. The annex declarations allow for the definition of~\cite{EMV1}:
\begin{enumerate}
\item Error types and type sets.
\item Error type mappings.
\item Error behavior state machines.
\item Error propagations and flows.
\item Component error behavior.
\item Composite error behavior.
\end{enumerate}
The extended linguistics of describing these facets are defined with the error model library. From a security standpoint this is advantageous because this allows developers to flag unexpected behavior or states that an attack might be able to take advantage of. From a developer's standpoint, the advantage is that in the early design phases not all actions or behavior may have been thoroughly documented or even planned out. While not purposed for security error-behavior, the tools can be improved to allow for the tracking of odd or unexpected security behavior that can be know from an early design phase.
The disadvantage of this being that while the error behavior can be modeled and verified, the security behavior of the system, and its components, is not readily tracked by this same tool and would require time and effort to implement and improve the language in a standardized manner.

Behavior Language for Embedded Systems with Software (BLESS) is a formal specification and verification tool purposed with formalizing the semantics of the existing Behavioral Annex (BA) sublanguage~\cite{BLESS2013}. If one defines AADL as a purely structure based language, BLESS is the user-community writing a language that is purely focused on behavior. The BLESS language works to mathematically define embedded programs, their specifications, and their executions from~\cite{BLESS2013}:
\begin{enumerate}
\item assertions to provide a formal behavior interface specification language.
\item annex subclauses for providing a formal component behavior language.
\item provide a proof tool that enables user of verification methods to show that model implementations meet defined system specifications with auditable evidence of compliance of the behaviors to specification.
\end{enumerate}
The act of proving that the system behavior and execution upholds defined specifications is done through the use of contracts defined for AADL component interfaces, descriptions of the internal component behaviors, and the annotation of programs using BLESS assertions to form `proof outlines'. These outlines can then be transformed, through the use of the proof tool, into proofs. BLESS was very much inspired by BA~\cite{BLESS2013}, and as such BLESS works to standardized not only the language but the process through the use of state-transition systems coupled with simple temporal logic formulas. To aid in BLESS' adoptability verification conditions are representation as a Hoare triple, allowing for use with other formal verification techniques. It is worth noting that the tool depends on the knowledge of the user and assumes that the proofs provided to the BLESS tool are inherently correct. With additional extension, BLESS can be tailored to allow for the tacking and proof-checking of security-centric behavior and execution of defined models. For example, mapping the behavior of authentication and authorization elements. In these cases a designer will need to define behavior for unexpected attempt to authorize or authenticate access rights. This behavior definition would then need to be definable as a set of Hoare triples for formal verification of secure system behavior. Coupling this work with the EMV2 AADL extension, a user could not only define the expected behavior and correctness of secure component execution, but also model the unexpected or strange behavior that an attacker would rely on for attacking a system. Unfortunately, BLESS is not focused on security behavior modeling and does not have the language necessary to begin describing security requirements of behavior.
The Error-Model Annex (EMV2) is purposed with tracking errors and their propagation throughout a system. The annex can also be used to describe component error behavior as transitions between different states, where transitions are triggered by error events and incoming propagations of error from other parts of the system design.
%The annex declarations allow for the definition of~\cite{EMV1}:
%\begin{enumerate}
% \item Error types and type sets.
% \item Error type mappings.
% \item Error behavior state machines.
% \item Error propagations and flows.
% \item Component error behavior.
% \item Composite error behavior.
%\end{enumerate}
%The extended linguistics of describing these facets are defined with the error model library. From a security standpoint this is advantageous because this allows developers to flag unexpected behavior or states that an attack might be able to take advantage of. From a developer's standpoint, the advantage is that in the early design phases not all actions or behavior may have been thoroughly documented or even planned out. While not purposed for security error-behavior, the tools can be improved to allow for the tracking of odd or unexpected security behavior that can be know from an early design phase.
The disadvantage of this annex is that while the error behavior can be modeled and verified, the security behavior of the system, and its components, is not readily tracked by this same tool and would require time and effort to implement and improve the language in a standardized manner.

Behavior Language for Embedded Systems with Software (BLESS) is a formal specification and verification tool purposed with formalizing the semantics of the existing Behavioral Annex (BA) sublanguage~\cite{BLESS2013}.
%If one defines AADL as a purely structure based language, BLESS is the user-community writing a language that is purely focused on behavior. The BLESS language works to mathematically define embedded programs, their specifications, and their executions from~\cite{BLESS2013}:
%\begin{enumerate}
% \item assertions to provide a formal behavior interface specification language.
% \item annex subclauses for providing a formal component behavior language.
% \item provide a proof tool that enables user of verification methods to show that model implementations meet defined system specifications with auditable evidence of compliance of the behaviors to specification.
%\end{enumerate}
%The act of proving that the system behavior and execution upholds defined specifications is done through the use of contracts defined for AADL component interfaces, descriptions of the internal component behaviors, and the annotation of programs using BLESS assertions to form `proof outlines'. These outlines can then be transformed, through the use of the proof tool, into proofs. BLESS was very much inspired by BA~\cite{BLESS2013}, and as such BLESS works to standardized not only the language but the process through the use of state-transition systems coupled with simple temporal logic formulas. To aid in BLESS' adoptability verification conditions are representation as a Hoare triple, allowing for use with other formal verification techniques. It is worth noting that the tool depends on the knowledge of the user and assumes that the proofs provided to the BLESS tool are inherently correct.
With additional extension, BLESS can be tailored to allow for the tacking and proof-checking of security-centric behavior and execution of defined models. For example, mapping the behavior of authentication and authorization elements. In these cases a designer will need to define behavior for unexpected attempt to authorize or authenticate access rights. This behavior definition would then need to be definable as a set of Hoare triples for formal verification of secure system behavior. Coupling this work with the EMV2 AADL extension, a user could not only define the expected behavior and correctness of secure component execution, but also model the unexpected or strange behavior that an attacker would rely on for attacking a system. Unfortunately, BLESS is not focused on security behavior modeling and does not have the language necessary to begin describing security requirements of behavior.

\subsection{AADL Security Annex Limitations}
Overall, the limitations of the current AADL security annex and analysis tools are that there is no focus on defining
Expand Down Expand Up @@ -303,7 +306,7 @@ Extensions to the security-centric aspects of the AADL language have been recent

% Add in an image of the drawing from the bulletjournal on the process
\begin{figure}
\includegraphics[width=\textwidth, height=8.8cm]{./images/aadl_security_framework.png}
\centering\includegraphics[height=6cm]{./images/aadl_security_framework.png}
\caption{Visualization of Security Framework}
\label{fig:AADLSecFrame}
\end{figure}
Expand Down Expand Up @@ -421,7 +424,8 @@ As can be seen in Figure~\ref{fig:AADLSecFrame} the power of this new framework


\subsection{Verification Tools}
Lastly, one will need to develop Resolute, or other annex tools, to account for security assurances through verification and validation solutions. Furthermore, standardization of the dialect must take place to allow for ease of communication of ideas, specifications, requirements, and expected behavior. Otherwise the advantages of this new security framework would not outweigh the cost and time spend learning the syntax and tools required.
When examining the security-based extensions to AADL, Resolute would make an effective method of verification and validation that a produced security model meets all of the required user-defined security assurances. These could range from networking connectivity requirements to dependencies on correctly implemented access control parameters. The disadvantgae of this tool, in its current state, is that the assurance checks are relatively simple and there has been little to no documentation on the user-community's efforts to improve the tool for security-centric applications of modeling.
Further work is needed to develop Resolute, or other annex tools, to account for security assurances through verification and validation solutions. Furthermore, standardization of the dialect must take place to allow for ease of communication of ideas, specifications, requirements, and expected behavior. Otherwise the advantages of this new security framework would not outweigh the cost and time spend learning the syntax and tools required.


% Mention how exploration of the entire design space is paramount to effective use of the framework; hence without a form of automation this tool can not be adequately used to generate secure model implemenations based on requirements and specifications.
Expand Down

0 comments on commit 2381918

Please sign in to comment.