diff --git a/AADLSecPaper.pdf b/AADLSecPaper.pdf index 2c50b64..6e05e04 100644 Binary files a/AADLSecPaper.pdf and b/AADLSecPaper.pdf differ diff --git a/AADLSecPaper.tex b/AADLSecPaper.tex index f484324..69df516 100644 --- a/AADLSecPaper.tex +++ b/AADLSecPaper.tex @@ -121,7 +121,7 @@ Although security was not an initial concern in the development of the AADL lang \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. +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 attack surface graphical representation \begin{figure} @@ -133,9 +133,16 @@ 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. 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, this paper will touch back upon Resolute's use for security requirement definition. +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. -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. +% 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. 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} @@ -146,7 +153,7 @@ The Error-Model Annex is purposed with tracking errors and their propagation thr \item Component error behavior. \item Composite error behavior. \end{enumerate} -The extended linguistics of describing these facets are defined with the error model library. As with all other aspects of AADL, this error model library can also be user extended to allow for new error types or even an extension of the error type hierarchy. In current examples~\cite{Osate2Examples} this annex is noted as `EMV2'. This is due to the development of the error-modeling annex to allow for both the original error-model annex and version 2 to co-exist~\cite{EMV2}. The advantage of this tool development is that a user can now define not only the architectural specifications of a design but also that systems behavior under unknown or unexpected conditions. Since AADL is originally focused on the architectural definition of modeled systems, the propagation paths of the error-modeling annex are determined by the architecture. 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. 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. +The extended linguistics of describing these facets are defined with the error model library. As with all other aspects of AADL, this error model library can also be user extended to allow for new error types or even an extension of the error type hierarchy. In current examples~\cite{Osate2Examples} this annex is noted as `EMV2'. This is due to the development of the error-modeling annex to allow for both the original error-model annex and version 2 to co-exist~\cite{EMV2}. The advantage of this tool development is that a user can now define not only the architectural specifications of a design but also that systems behavior under unknown or unexpected conditions. Since AADL is originally focused on the architectural definition of modeled systems, the propagation paths of the error-modeling annex are determined by the architecture. 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. This annex would allow for planning on possible behavioral complications that would produce errors or cause a system to no longer function correctly. For example, how should a modeled security system behave if a client does not have any of the encryption or authentication methods that a server relies on to maintain a secure and protected connection. 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. In fact, BLESS programs are attached to system architectures to define component behavior because the community felt that AADL lacked a formal behavior interface specification language, needed a formal component behavior language, and required a set of verification methods and tools to ensure compliance of behavior implementation meeting specifications of the model. The BLESS language works to mathematically define embedded programs, their specifications, and their executions from~\cite{BLESS2013}: \begin{enumerate} @@ -154,7 +161,7 @@ Behavior Language for Embedded Systems with Software (BLESS) is a formal specifi \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 specification is done through the use of contracts define 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 while BLESS' proof tool will verify conditions generated through AADL and check existing proofs, it is by not means a tool for proving theorems. In other words, the tool depends on the knowledge of the user and assumes that the proofs provided to the BLESS tool are inherently correct. Current work on development and improvement of the tool include working towards augmenting BLESS behavioral models with EMV2 error models along with adding simulation and code generation to the list of capabilities. From a security viewpoint, this tool allows for a more complete description and verification of component and system behavior. With additional extension, BLESS can be tailored to allow for the tacking and proof-checking of security-centric behavior and execution of defined models. This would greatly aid in making AADL a standard for security behavior and requirement specification design. 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. This combination of efforts would allow for a far better modeling and mapping of the entire system behavior under secure conditions. Unfortunately, BLESS is not focused on security behavior modeling and does not have the language necessary to begin describing security requirements of behavior. +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 while BLESS' proof tool will verify conditions generated through AADL and check existing proofs, it is by not means a tool for proving theorems. In other words, the tool depends on the knowledge of the user and assumes that the proofs provided to the BLESS tool are inherently correct. Current work on development and improvement of the tool include working towards augmenting BLESS behavioral models with EMV2 error models along with adding simulation and code generation to the list of capabilities. From a security viewpoint, this tool allows for a more complete description and verification of component and system behavior. 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. The next step is developing a method for converting requirements and component definitions into a Hoare triple type notation for use with known formal verification methods. This would greatly aid in making AADL a standard for security behavior and requirement specification design. 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. This combination of efforts would allow for a far better modeling and mapping of the entire system behavior under secure conditions. 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} Taking a deeper look at these developments for the AADL language, there are certain improvements that this paper @@ -196,6 +203,8 @@ A prime example this is the act of deciding to use key generation for authentica \end{enumerate} No where in this process is trust seen as a non-binary aspect. One can not say that they trust a component 80\% of the time, but they can say that they will trust a component if it is reliable 80\% of the time. In this sense, it is the deep held belief of this paper that trust should be a binary value (trusted or not trusted) while reliability can act as a supplementary value that acts as the `error bounds' by which trust is bestowed or given. A combination or mapping of trust and reliability can be given to produce a value of `component correctness', similar to how exposure is defined. +AADL is indeed a powerful and versatile language that has the potential to also act as an effective method of secure real-time embedded system design. While there has been work towards developing and improving the lack of a formalized security annex, even this work will still require the use, frustration, and feedback of the user-community to help establish a standardized tool. The greatest inadequacy of the lexicon is that there is currently no attention being given to the description and definition of high level security requirements and lower level secure component definitions that are required in order to establish and mature a tool for secure embedded system model generation and verification. While the building blocks of an effective security framework have begun to appear, there is still the need for a standardized and formal security framework in the AADL language. + \section{Proposed Extensions to AADL} \label{New Framework} % Add in an image of platform-based design to illustrate the refinement process @@ -209,7 +218,7 @@ While extensions to the security-centric aspects of the AADL language have been % Add in an image of the drawing from the bulletjournal on the process \begin{figure} - \includegraphics[width=\textwidth]{./images/aadl_security_framework.png} + \includegraphics[width=\textwidth, height=10cm]{./images/aadl_security_framework.png} \caption{Visualization of Security Framework} \label{fig:AADLSecFrame} \end{figure} @@ -223,7 +232,7 @@ The new security framework that this paper proposes would require the following \end{enumerate} Other additional aspects of this framework, that could come from the existing tools, extensions, and annexes would include code generated using the secure models. %An advantage of this framework is that it borrows from the platform-based design model, shown in Figure~\ref{fig:RecursivePBD}, allowing for continual refinement and improvement of designs while also improving early phase development of new components and systems. -As can be seen in Figure~\ref{fig:AADLSecFrame} the power of this new framework comes from the mapping process used to combine the component definitions and requirements as well as the verification of the mapping instances. However, before those aspects of the framework can be formalized, one must first have clarification of the language used to define and describe component specifications and requirements of the system. Furthermore, standardization of the dialect must take place to allow for ease of communication of ideas, specifications, requirements, and expected behavior. +As can be seen in Figure~\ref{fig:AADLSecFrame} the power of this new framework comes from the mapping process used to combine the component definitions and requirements as well as the verification of the mapping instances. However, before those aspects of the framework can be formalized, one must first have clarification of the language used to define and describe component specifications and requirements of the system. For AADL to become the descriptive language for this sort of framework, one will need to first define a secure device library that will represent common implementations of known secure system models. From here one will then need to produce a manner of combining existing constraint linguistics with security needs to produce comparable, quantitative security metrics for both functional and non-functional behavior and security requirements. 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. % Add in the table of elements and variations \begin{table*}[] diff --git a/images/resoluteExample.png b/images/resoluteExample.png new file mode 100644 index 0000000..e98f57e Binary files /dev/null and b/images/resoluteExample.png differ