diff --git a/AADLSecPaper.tex b/AADLSecPaper.tex index 69df516..e3feeb2 100644 --- a/AADLSecPaper.tex +++ b/AADLSecPaper.tex @@ -18,6 +18,44 @@ \usepackage{graphicx} %\usepackage{graphics} +\usepackage{listings} % Include the listings-package +\usepackage{color} +\usepackage{balance} +\useunder{\uline}{\ul}{} + +\definecolor{darkgreen}{rgb}{0,0.5,0} +\definecolor{mygreen}{rgb}{0,0.6,0} +\definecolor{mygray}{rgb}{0.5,0.5,0.5} +\definecolor{mymauve}{rgb}{0.58,0,0.82} +\lstset{ % + backgroundcolor=\color{white}, % choose the background color; you must add \usepackage{color} or \usepackage{xcolor} + basicstyle=\ttfamily\scriptsize, % the size of the fonts that are used for the code + breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace + breaklines=true, % sets automatic line breaking + captionpos=b, % sets the caption-position to bottom + commentstyle=\color{mygreen}, % comment style + deletekeywords={...}, % if you want to delete keywords from the given language + escapeinside={\%*}{*)}, % if you want to add LaTeX within your code + extendedchars=true, % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8 + frame=single, % adds a frame around the code + keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible) + keywordstyle=\color{blue}, % keyword style +% language=C, % the language of the code + morecomment=[l]{--}, + morekeywords={property,set,is,type, constant, enumeration, end, applies, to, inherit, of, *,...}, % if you want to add more keywords to the set + numbers=left, % where to put the line-numbers; possible values are (none, left, right) + numbersep=5pt, % how far the line-numbers are from the code + numberstyle=\tiny\color{mygray}, % the style that is used for the line-numbers + rulecolor=\color{black}, % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here)) + showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces' + showstringspaces=false, % underline spaces within strings only + showtabs=false, % show tabs within strings adding particular underscores + stepnumber=1, % the step between two line-numbers. If it's 1, each line will be numbered + stringstyle=\color{mymauve}, % string literal style + tabsize=2, % sets default tabsize to 2 spaces + title=\lstname % show the filename of files included with \lstinputlisting; also try caption instead of title +} + \begin{document} \title{AADL Language Review and Expansion with Respect to Security Behavior and Requirements} @@ -105,23 +143,43 @@ 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 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. +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 Listing~\ref{lst: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. -% 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} +\begin{lstlisting}[caption={User-defined AccessMode and AccessGroup properties~\cite{ellison2015extending}},label={lst:AADLaccessExtension}] +property set Security_Trust is -% 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} +-- properties to support documenting and analyzing security +-- Added property that supports access mode of data + + AccessProtection: list of record ( + + ) applies to (all); + +end Security_Trust; +\end{lstlisting} + +%% 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} + +\begin{lstlisting}[caption={Security Level Definition for AADL Security Annex~\cite{AADLSecAnnex}},label={lst:AADLSecLevels}] +security_levels : list of aadlinteger => (100) applies to (all); +top_secret : constant aadlinteger => 10; +secret : constant aadlinteger => 40; +unclassified : constant aadlinteger => 100; +\end{lstlisting} -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. Unfortunately not much has been released on implementation examples of the new security annex and analysis tools as improvement is expected to continue through June 2016 with an official publication to the SEI github in July 2016~\cite{AADLSecAnalysis}. +%% 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 Listing~\ref{lst: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. Unfortunately not much has been released on implementation examples of the new security annex and analysis tools as improvement is expected to continue through June 2016 with an official publication to the SEI github in July 2016~\cite{AADLSecAnalysis}. % Add in an image of attack surface graphical representation \begin{figure} @@ -133,14 +191,15 @@ More current work on the development of a security annex for AADL has been relea \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. -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. +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. -% Add in an image of resolute being used as a security verification tool -\begin{figure} - \includegraphics[width=\textwidth]{./images/resoluteExample.png} - \caption{Example of Resolute as a Security Property Verification Tool~\cite{ellison2015extending}} - \label{fig:AADLResoluteExample} -\end{figure} +%% Add in an image of resolute being used as a security verification tool +%\begin{figure} +% \includegraphics[width=\textwidth]{./images/resoluteExample.png} +% \caption{Example of Resolute as a Security Property Verification Tool~\cite{ellison2015extending}} +% \label{fig:AADLResoluteExample} +%\end{figure} 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}. This allows 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. As with the Resolute tool, RDALTE allows for effective implementation and verification of system requirement definition and analysis but is not primarily focused on security requirements or constraints. Though, as with all extensions and plug-in of AADL, it is possible for a user to expand on the existing tool to be able to handle security needs. 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. @@ -172,7 +231,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. An example of this type of definition is given in Figure~\ref{fig:AADLSecEncryption}. 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 Listing~\ref{lst: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, @@ -189,12 +248,31 @@ and validation of security requirements and behavior. While having the language 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} +\begin{lstlisting}[caption={AADL Security Annex Definitions of Encryption~\cite{AADLSecAnnex}},label={lst:AADLSecEncryption}] +encryption : security_properties::encryption_type applies to + {port, virtual bus, bus, memory, access}; +encryption_type : type record ( + method : security_properties::supported_encryption_method; + algorithm : security properties::supported_encryption_algorithm; + public_key : aadlstring; + private_key : aadlstring; + key : aadlstring; + operation_mode : security_properties::supported_operation_mode; +}; +supported_encryption_method : + type enumeration (symetric, assymetric, clear); +supported_encryption)algorithm : + type enumeration (tripledes, des, rsa, blowfish, aes, clear); +supported_operations_mode : + type enumeration (ecb, cbc, pcbc, cfb, ofb, ctr); +\end{lstlisting} + +%% 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}