diff --git a/AADLSecPaper.tex b/AADLSecPaper.tex index e3b2073..b9131c2 100644 --- a/AADLSecPaper.tex +++ b/AADLSecPaper.tex @@ -64,7 +64,7 @@ % also used for the TOC unless % \toctitle is used % -\author{Paul Wortman \and John Chandy} +%\author{Paul Wortman \and John A. Chandy} % %\authorrunning{Ivar Ekeland et al.} % abbreviated author list (for running head) % @@ -97,7 +97,8 @@ The Architecture Analysis \& Design Language (AADL) is an architecture descripti Recent work on extending AADL's capabilities and tools has ranged from the development of error tracking, behavioral descriptions and definitions, code generation, requirement modeling, security description and definition, as well as verification of proposed system models and implementations. With such research and effort being poured into the many facets of the language, AADL is becoming a more powerful and well rounded tool. Due to the ease by which new extensions and user-define additions can be created for AADL, the community is greatly responsible for the development and improvement of AADL as a modeling and analysis tool. More on these annexes and extensions will be examined in Section ~\ref{AADL Annexes and Extensions} along with their affect on the overall use and growth on the tools use and potential. \label{securityBasics} -Secure systems design is a formidable and troublesome obstacle that is not well understood and even more poorly implemented. From examples of Jeep Cherokee's security weaknesses~\cite{jeepHack}, airplane hacker scares~\cite{planeHack}, adware implementation weaknesses~\cite{superFish}\cite{lenovoWPBT}, government employee data breaches~\cite{govHack}, code implementation concerns~\cite{stageFright}, and other update security concerns~\cite{googleAndroid, androidMarshmallow} one can see that a lack of standardized security design and implementation can render catastrophic failure. This issue is further exacerbated by how vast the problem space is (e.g. secure software, trusted platform modules, new authentication methods)~\cite{aaraj2008analysis,denning1996location,%mapayi2013evaluating, lin2015security, shi2013new, son2015software, +Secure systems design is a formidable and troublesome obstacle that is not well understood and even more poorly implemented. From examples of Jeep Cherokee's security weaknesses~\cite{jeepHack}, airplane hacker scares~\cite{planeHack}, adware implementation weaknesses~\cite{superFish}\cite{lenovoWPBT}, government employee data breaches~\cite{govHack}, code implementation concerns~\cite{stageFright}, and other update security +concerns~\cite{androidMarshmallow,googleAndroid} one can see that a lack of standardized security design and implementation can render catastrophic failure. This issue is further exacerbated by how vast the problem space is (e.g. secure software, trusted platform modules, new authentication methods)~\cite{aaraj2008analysis,denning1996location,%mapayi2013evaluating, lin2015security, shi2013new, son2015software, saito2015case,denning2015toward,nguyen2015model,ravi2004security,gokhale2008model,perez2006vtpm,yan2015novel,tehranipoor2015dram}. Security is always evolving as knowledge @@ -194,7 +195,7 @@ Other additions to the language include the definition of domains (e.g. entertai \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}. 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}. +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}. 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. %% Add in an image of resolute being used as a security verification tool @@ -204,7 +205,7 @@ Resolute is a language and tool for developing architectural assurance cases~\ci % \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}; 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 Requirements Definition and Analysis Language Tool Environment \linebreak(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 (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}: @@ -251,7 +252,7 @@ library is two-fold. The first issue is that in order for a security implement 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}\cite{jurjens2005secure}. This reliance on the knowledge and expertise of +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} @@ -273,7 +274,7 @@ encryption_type : type record ( operation_mode : security_properties::supported_operation_mode; }; supported_encryption_method : - type enumeration (symetric, assymetric, clear); + type enumeration (symmetric, asymmetric, clear); supported_encryption)algorithm : type enumeration (tripledes, des, rsa, blowfish, aes, clear); supported_operations_mode : @@ -287,12 +288,12 @@ supported_operations_mode : % \label{fig:AADLSecEncryption} %\end{figure} -A prime example 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: +A prime example is the act of deciding to use hardware-based 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? + \item Does the generated key have enough bits to be useful for current day implementations of algorithms and methods? \item Can I trust said component to reliably generate the same key under the same conditions? \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. +Nowhere 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. @@ -306,7 +307,7 @@ The greatest inadequacy of the lexicon is that there is currently no attention b % \label{fig:RecursivePBD} %\end{figure} -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. Even more of a void can be felt for a set of automated tools for exploring the security design space. +As explained above, 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. Even more of a void can be felt for a set of automated tools for exploring the security design space. % Add in an image of the drawing from the bulletjournal on the process \begin{figure} @@ -386,16 +387,18 @@ end procbase.encryptembedded_i; Once separate libraries of components and potential security requirements have been produced, the next step would be to formalize a method for being able to compare and contrast both the functional and non-functional requirements of the system to existing component -solutions. Listing~\ref{lst:AADLUserDefineHigh} shows an example of how AADL could be used to specify security requirements. One will need to first define a secure device library that will represent common implementations of known secure system models, along with providing detailed descriptions of qualitative requirements that must be met (and checked) by a design or development team. 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. +solutions. +One will need to first define a secure device library that will represent common implementations of known secure system models, along with providing detailed descriptions of qualitative requirements that must be met (and checked) by a design or development team. 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. Once one has defined these comparable security metrics, it is possible to develop a mapping process that will not only account for the needs of the modeled system but also take into account the constraints of embedded systems. These constraints will originate both from the user-defined requirements and needs of the system, but also from the architectural limitations of the components available to form the base of the existing design space. Additionally the security constraints of a given design need to be based on something more -concrete than a 0 to 100 scale. It is possible that the more subjective design requirements will need more of a goal-evidence-justification style verification outline as seen in more recent work done for the Architecture Led Incremental System Assurance (ALISA) approach~\cite{ALISA2016}. Requirements must be defined via a metric derived from costs and values that -represent the core elements being protected, how these components must be protected, and the standards that must +concrete than a 0 to 100 scale. Requirements should be defined via a metric derived from costs and values that +represent the core elements being protected, the inherent risk of vulnerabilities associated with these elements, and the standards that must be met by a given implementation. - +Listing~\ref{lst:AADLUserDefineHigh} shows an example of how AADL could be used to specify security requirements. Security requirements are specified in terms of value of a service feature and impact of the feature if it was to be compromised. +It is possible that the more subjective design requirements will need more of a goal-evidence-justification style verification outline as seen in more recent work done for the Architecture Led Incremental System Assurance (ALISA) approach~\cite{ALISA2016}. \begin{lstlisting}[caption={User-defined Higher Level Security Requirement},label={lst:AADLUserDefineHigh}] abstract implementation sysreq.wireless_sensor_i @@ -421,14 +424,14 @@ abstract implementation sysreq.wireless_sensor_i end sysreq.wireless_sensor_i; \end{lstlisting} -\subsection{Mapping Tools} +\subsection{Mapping Process} %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. The mapping process requires the implementation of automated tools for the purpose of thoroughly exploring the entire design space for optimizing generated designs while minimizing the amount of time spent developing said design models. But before an automated process can be constructed, one has to first define the parameters that will be used for describing the constraints, requirements, and capabilities of a design. From these values, the mapping would generate new instances of design solutions that would later need use of verification and validation tools to ensure that produced implementations of security models still meet all user-defined constraints and needs. \subsection{Verification Tools} -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. An example of one such security check is shown by Listing~\ref{lst:AADLUserDefineResolute}; examining that all connections between given components maintain an expectation of encryption. +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 disadvantage 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. An example of one such security check is shown by Listing~\ref{lst:AADLUserDefineResolute}; examining that all connections between given components maintain an expectation of encryption. \begin{lstlisting}[caption={User-defined Resolute Checks},label={lst:AADLUserDefineResolute}] package arch_resolute_checks