Images added to paper showing implementations of the AADL Security Annex

AADLSecPaper.tex

@@ -105,9 +105,30 @@ Using these various core elements of the AADL language a designer is capable of
 \subsection{AADL Security Annex}
 
 % December 2015 Security Work
-Although security was not an initial concern in the development of the AADL language, there has been work made to extend the language to include behavioral and security-centric capabilities.  Recent work by Ellison et.~al.~\cite{ellison2015extending} has extended the security centric properties of AADL to include user-defined `AccessGroup' and `AccessMode' properties that are used for evaluating and validating an existing system model.  The extension adds different security types (e.g. unclassified, confidential, secret, top secret).  When implementing these extended security properties, one must determine the viability of a system given confidentiality requirements of data objects and security clearance by users.  These security extensions allow for analysis of the modeled system to ensure processes and threads are mapped to appropriate hardware, communicate over secured channels, and store data in protected memory.  It also allows one to derive minimum security requirements on hardware components given a software architecture.  While these two properties are effective at validating that a system will retain some arbitrary level of security, this is still not the level of detail that effectively allows for modeling of component specifications.
+Although security was not an initial concern in the development of the AADL language, there has been work made to extend the language to include behavioral and security-centric capabilities.  Recent work by Ellison et.~al.~\cite{ellison2015extending} has extended the security centric properties of AADL to include user-defined `AccessGroup' and `AccessMode' properties that are used for evaluating and validating an existing system model based on user expectations of functionality, as shown in Figure~\ref{fig:AADLaccessExtension}.  The extension adds different security types (e.g. unclassified, confidential, secret, top secret).  When implementing these extended security properties, one must determine the viability of a system given confidentiality requirements of data objects and security clearance by users.  These security extensions allow for analysis of the modeled system to ensure processes and threads are mapped to appropriate hardware, communicate over secured channels, and store data in protected memory.  It also allows one to derive minimum security requirements on hardware components given a software architecture.  While these two properties are effective at validating that a system will retain some arbitrary level of security, this is still not the level of detail that effectively allows for modeling of component specifications.
 
-More current work on the development of a security annex for AADL has been released~\cite{AADLSecAnnex}.  The concept behind this work is to extend the AADL language with a series of security annotations that will represent the security characteristics in designed architecture models.  In comparison to the earlier work by Ellison et.~al.~, there is still the existence of `Security Levels' (e.g. unclassified, secret, top secret) but there are now integer values associated with each level.  According to the information provided during the May 2016 User Days, this allows for greater compliance with other approaches such as Bell-Lapadula~\cite{AADLSecAnnex}.  Other additions to the language include the definition of domains (e.g. entertainment, command and control), a level of trust, a degree of exposure, along with enumerated definitions of encryption methods and properties as well as authentication methods and implementations.  In terms of security analysis tools, there has been work towards defining the attack surface in terms of how vulnerabilities are discovered within the architecture and a measurement of how safe a system is.  Along the same vein, there has also been work toward generating graphical representation of vulnerabilities and their impact upon the system; similar in nature to failure mode and effect analysis or fault tree analysis.  A more interesting development has been for including code generation for secure microkernel architectures such as the seL4.
+% Add in an image of access mode and group extensions
+\begin{figure}
+	\includegraphics[width=\textwidth]{./images/accessModeGroupExample.png}
+	\caption{User-defined AccessMode and AccessGroup properties~\cite{ellison2015extending}}
+	\label{fig:AADLaccessExtension}
+\end{figure}
+
+% Add in an image of new security level extensions
+\begin{figure}
+	\includegraphics[width=\textwidth]{./images/securityLevelsExample.png}
+	\caption{Security Level Definition for AADL Security Annex~\cite{AADLSecAnnex}}
+	\label{fig:AADLSecLevels}
+\end{figure}
+
+More current work on the development of a security annex for AADL has been released~\cite{AADLSecAnnex}.  The concept behind this work is to extend the AADL language with a series of security annotations that will represent the security characteristics in designed architecture models.  In comparison to the earlier work by Ellison et.~al.~, there is still the existence of `Security Levels' (e.g. unclassified, secret, top secret) but there are now integer values associated with each level, as shown in Figure~\ref{fig:AADLSecLevels}.  According to the information provided during the May 2016 User Days, this allows for greater compliance with other approaches such as Bell-Lapadula~\cite{AADLSecAnnex}.  Other additions to the language include the definition of domains (e.g. entertainment, command and control), a level of trust, a degree of exposure, along with enumerated definitions of encryption methods and properties as well as authentication methods and implementations.  In terms of security analysis tools, there has been work towards defining the attack surface in terms of how vulnerabilities are discovered within the architecture and a measurement of how safe a system is.  An example of this is shown in Figure~\ref{fig:AADLAttackAnalysis}.  Along the same vein, there has also been work toward generating graphical representation of vulnerabilities and their impact upon the system; similar in nature to failure mode and effect analysis or fault tree analysis.  A more interesting development has been for including code generation for secure microkernel architectures such as the seL4.
+
+% Add in an image of attack surface graphical representation
+\begin{figure}
+	\includegraphics[width=\textwidth, height=6cm]{./images/attackAnalysis.png}
+	\caption{Graphical Example of AADL Security Annex Attack Impact Analysis~\cite{AADLSecAnalysis}}
+	\label{fig:AADLAttackAnalysis}
+\end{figure}
 
 \subsection{AADL Tools support for Security}
 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.
@@ -144,7 +165,7 @@ possibility of attack on a specific element within a design.  Both of these addi
 to formalize a verification of potential security hazards and complications that may arise further down the 
 development cycle or even once out in the field.  Other additions to the AADL lexicon, such as the encryption 
 and authentication descriptions, require that a form of library be written to allow for proper description and 
-definition of the security-based algorithms and methods being used by different components of a system.  From a 
+definition of the security-based algorithms and methods being used by different components of a system.  An example of this type of definition is given in Figure~\ref{fig:AADLSecEncryption}.   From a 
 network standpoint this is highly advantageous because this also allows for a formal set of verification tools 
 that standards and expectations are being met by all components of the design.  The disadvantage of such a 
 library is two-fold.  The first issue is that in 	order for a security implementation library to be generated, 
@@ -160,6 +181,14 @@ merging of concepts does not accurately reflect security concerns and does not a
 and validation of security requirements and behavior.  While having the language to describe and define the 
 correctness of a component is advantageous, this is not the same as trust but should rather be seen as a 
 combination of trust and reliability.  
+
+% Add in an image of attack surface graphical representation
+\begin{figure}
+	\includegraphics[width=\textwidth]{./images/encryptionExample.png}
+	\caption{AADL Security Annex Definitions of Encryption~\cite{AADLSecAnnex}}
+	\label{fig:AADLSecEncryption}
+\end{figure}
+
 A prime example this is the act of deciding to use key generation for authentication versus encryption.  In this scenario there is a need to know that the key generated is reliable to a given percentage (e.g. 99.9\% versus 99.999\%).  If one attempts to describe the key generation process, or even validate it's use for one given role or another, a security expert should have two questions in mind:
 \begin{enumerate}
 	\item Does the key generated have enough bits to be useful for current day implementations of algorithms and methods?
@@ -310,6 +339,11 @@ Delange, J., Feiler, P., Klieber, W., Nam, M., Seibel, J.:
 AADL Security Annex,
 \url{https://github.com/saeaadl/userdays/blob/master/UserDays/May2016/security-annex-May2016.pdf}
 
+\bibitem {AADLSecAnalysis}
+Delange, J., Nam, M., Seibel, J.:
+AADL Security Analysis Tools,
+\url{https://github.com/saeaadl/userdays/blob/master/UserDays/May2016/security-analysis-May2016.pdf}
+
 \bibitem {ellison2015extending}
 Ellison, R., Householder, A., Hudak, J., Kazman, R., Woody, C.:
 Extending AADL for Security Design Assurance of Cyber-Physical Systems,