diff --git a/AADLSecPaper.tex b/AADLSecPaper.tex index d0bcd59..0426db5 100644 --- a/AADLSecPaper.tex +++ b/AADLSecPaper.tex @@ -45,7 +45,11 @@ \maketitle % typeset the title of the contribution \begin{abstract} -AADL is a common use language that has been developed and tweaked over the year to alloow the ability to describe model behavior and specifications, with more recent attempts to define language for security requirements and verification. This paper examines previous implementations of behavior, requirements, and security in AADL and then goes to propose a new framework for better integration and description of security requirements and behavior within the AADL lexicon. +AADL is a common use language that has been developed and tweaked over the years to allow the ability to +describe model behavior and specifications, with more recent attempts to define language for security +requirements and verification. This paper examines previous implementations of behavior, requirements, and +security in AADL and then goes to propose a new framework for better integration and description of security +requirements and behavior within the AADL lexicon. \keywords{security modeling, security framework} \end{abstract} @@ -85,6 +89,7 @@ So why should an individual choose to use AADL rather than any of the other desc \section{AADL Annexes and Security Extensions} \label{AADL Annexes and Extensions} +\subsection{Introduction to AADL} The Architecture Analysis \& Design Language (AADL) is traditionally design for the specification, analysis, automated integration and code generation of real-time performance-critical distributed computer systems~\cite{AADLSite}. The `performance-critical' aspects of a system include timing, safety, schedulability, fault tolerance, and security. AADL works to provide a new language vehicle for allowing analysis of system designs prior to development. This language also supports model-based, model-driven development of designs throughout the life-cycle of a system or system-of-systems. The advantage being that the language and associated tools allow for developers to model, analyze, and generate embedded real-time systems while supporting model-based engineering concepts. The AADL lexicon allows for the following aspects to be described~\cite{AADLV2Overview}: \begin{enumerate} \item Precise execution semantics for components. These components are thread, process, data, subprogram, system, processor, memory, bus, device, virtual processor, virtual bus. @@ -95,8 +100,16 @@ The Architecture Analysis \& Design Language (AADL) is traditionally design for \end{enumerate} Using these various core elements of the AADL language a designer is capable of describing not only the higher level abstractions of a system, network, or system-of-systems, but is also able to define individual components or system-on-a-chip (SoC) down to the connections, subcomponents, or even arbitrary user-define properties. The aspect of extensibility and accommodation to the needs of a user is what allows for AADL to excel at a wide variety of tasks. Furthermore, this same aspect allows for the standardization of these extensions in the form of annexes. The large user community lends to the vetting of these additions to the language as well as refinement of the lexicon. Due to AADL's wide adoption and use in real-time embedded system design, there is a large-scale of available tools already developed by the user community~\cite{AADLTools}. The rest of this section will be devoted to examining the existing community tools and their effect on AADL's ability to represent the security behavior and requirements of current day real-time embedded system design. -The first tool worth examining is `Osate 2'. This is an open-source tool platform used to support AADL v2~\cite{Osate2}. Its intention is for both end users and tool developers by providing a complete textual editor for the AADL language along with a simple set of analysis tools. It also makes use of the Eclipse platform to provide support for the AADL meta model. Included with the graphical editor and code generation capability is the capability to extend the tools with additional plug-ins, both official and user-defined variations. Through Osate 2, members of the AADL community can produce patches to existing extensions, report bugs with current implementations, and prepare their own releases of new augmentations of the lexicon or even entire annexes for community use. As a standalone java application, Osate 2 provides an ease of adoptability when learning the language and a relatively small requirement for installation. Although this is an effective tool for consolidating AADL and its plug-ins, Osate 2 does not directly affect changes or alterations to the AADL language but only allows for greater ease of use. However, as a base for further development of AADL it is remarkably efficient. +%The first tool worth examining is `Osate 2'. This is an open-source tool platform used to support AADL v2~\cite{Osate2}. Its intention is for both end users and tool developers by providing a complete textual editor for the AADL language along with a simple set of analysis tools. It also makes use of the Eclipse platform to provide support for the AADL meta model. Included with the graphical editor and code generation capability is the capability to extend the tools with additional plug-ins, both official and user-defined variations. Through Osate 2, members of the AADL community can produce patches to existing extensions, report bugs with current implementations, and prepare their own releases of new augmentations of the lexicon or even entire annexes for community use. As a standalone java application, Osate 2 provides an ease of adoptability when learning the language and a relatively small requirement for installation. Although this is an effective tool for consolidating AADL and its plug-ins, Osate 2 does not directly affect changes or alterations to the AADL language but only allows for greater ease of use. However, as a base for further development of AADL it is remarkably efficient. +\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. + +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. + +\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, 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. @@ -122,12 +135,31 @@ Behavior Language for Embedded Systems with Software (BLESS) is a formal specifi \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. -% 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. - -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. - -Taking a deeper look at these developments for the AADL language, there are certain improvements that this paper believes are a step in the right direction. Including a numerical value to `security levels' allows for quantitative analysis of this property through a system's design. The concept of exposure (e.g. how exposed a component or system is) is brilliant and coupled with a numerical value allows for a security metric for determining the possibility of attack on a specific element within a design. Both of these additional properties open the door 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 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, one must rely on the knowledge of a `security expert' or `security experts' to define all the possible combinations and implementations that are currently in use. The second problem being the need to maintain such a record in a formal and standardized method. While not an impossible task, this is an issue that has plagued this sort of work~\cite{jurjens2002umlsec, jurjens2005secure}. This reliance on the knowledge and expertise of individuals may not be avoidable, in which case the current solution may be the best at hand, but is by no means a poor answer to a long standing problem. The one addition that this paper does not agree with is the move to describe the security aspect of `trust' as a non-binary value. While the released work~\cite{AADLSecAnnex} states that this scale is representative of proof of a component's correctness, this paper believes that this merging of concepts does not accurately reflect security concerns and does not allow for accurate verification 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. +\subsection{AADL Security Annex Limitations} +Taking a deeper look at these developments for the AADL language, there are certain improvements that this paper +believes are a step in the right direction. Including a numerical value to `security levels' allows for +quantitative analysis of this property through a system's design. The concept of exposure (e.g. how exposed a +component or system is) coupled with a numerical value allows for a security metric for determining the +possibility of attack on a specific element within a design. Both of these additional properties open the door +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 +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, +one must rely on the knowledge of a `security expert' or `security experts' to define all the possible +combinations and implementations that are currently in use. The second problem being the need to maintain such +a record in a formal and standardized method. While not an impossible task, this is an issue that has plagued +this sort of work~\cite{jurjens2002umlsec, jurjens2005secure}. This reliance on the knowledge and expertise of +individuals may not be avoidable, in which case the current solution may be the best at hand, but is by no means +a poor answer to a long standing problem. The one addition that this paper does not agree with is the move to +describe the security aspect of `trust' as a non-binary value. While the released work~\cite{AADLSecAnnex} +states that this scale is representative of proof of a component's correctness, this paper believes that this +merging of concepts does not accurately reflect security concerns and does not allow for accurate verification +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. 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? @@ -135,14 +167,14 @@ 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. -\section{New Framework} +\section{Proposed Extensions to AADL} \label{New Framework} % Add in an image of platform-based design to illustrate the refinement process -\begin{figure} - \includegraphics[width=\textwidth]{./images/recursivePBD.png} - \caption{Visualization of Recursive PBD Model~\cite{sangiovanni2007quo}} - \label{fig:RecursivePBD} -\end{figure} +%\begin{figure} +% \includegraphics[width=\textwidth]{./images/recursivePBD.png} +% \caption{Visualization of Recursive PBD Model~\cite{sangiovanni2007quo}} +% \label{fig:RecursivePBD} +%\end{figure} While extensions to the security-centric aspects of the AADL language have been recently released but the focus of these linguistic extensions is for system analysis and code generation while not focusing on low level element properties and how to map them to higher level system requirements. As such, this paper proposes a security framework that can be adopted as an extension to AADL for the purpose of creating security model implementations mapped from security requirements and component specifications. Having examined the previous work and development of the AADL language, one can see that there is concurrent effort being placed in tracking different areas of real-time embedded system design, such as error propagation, behavior of systems and components, as well as the definition and validation of requirements. Although these extensions and annexes are not tailored specifically for security modeling needs and purposes, AADL allows for their combined use to help fill in the gaps of security requirement definition and behavior under different scenarios and conditions. The one `disadvantage' being that users will need to learn each tool separately and will be left to discover the best method of aggregate implementation; although this is truly the advantage of AADL as its own language. Considering the declared additions of a security annex extension to the AADL lexicon, there is an expansion for being able to describe said properties and aspects, but no movement yet towards verification of requirements and needs as seen with other annexes (e.g. RDALTE). There is notable work towards graphical representations of these security aspects, but again there is still a gap for the generation of secure system implementations and models. @@ -160,7 +192,9 @@ The new security framework that this paper proposes would require the following \item Creation of a mapping process by which security requirements and secure component specifications can be uniformly compared to allow for the generation of potential secure architectural system model solutions to the given inputs. \item Verification tools to validate mapping implementation solutions. \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. +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. % Add in the table of elements and variations \begin{table*}[]