diff --git a/AADLSecPaper.tex b/AADLSecPaper.tex index 6b43cc3..489b0a4 100644 --- a/AADLSecPaper.tex +++ b/AADLSecPaper.tex @@ -97,8 +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}\cite{denning1996location} %mapayi2013evaluating, lin2015security, shi2013new, son2015software, -\cite{saito2015case}\cite{denning2015toward}\cite{nguyen2015model}\cite{ravi2004security}\cite{gokhale2008model}\cite{perez2006vtpm}\cite{yan2015novel}\cite{tehranipoor2015dram}. +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, +saito2015case,denning2015toward,nguyen2015model,ravi2004security,gokhale2008model,perez2006vtpm,yan2015novel,tehranipoor2015dram}. Security is always evolving as knowledge of encryption techniques, authentication technologies, access control methods and other security mechanisms change over @@ -310,14 +310,39 @@ Extensions to the security-centric aspects of the AADL language have been recent The new security framework that this paper proposes would require the following steps to take place: \begin{enumerate} - \item Creation of a low-level component library that would contain normal and secure version implementations of each base component within the architectural space used for model generation. (Example: Listing~\ref{lst:AADLUserDefineLow}) - \item Formalized description and definition of higher level security requirements that may come from user-defined needs or from the experience of knowledge of security experts. (Example: Listing~\ref{lst:AADLUserDefineHigh}) + \item Creation of a low-level component library that would contain normal and secure version implementations of each base component within the architectural space used for model generation. + \item Formalized description and definition of higher level security requirements that may come from user-defined needs or from the experience of knowledge of security experts. \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. - \item 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. \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. Work towards developing these sorts of tools for secure architectures (e.g. seL4) is already one of the focuses of current AADL security annex work~\cite{AADLSecAnalysis}. +\subsection{Component Libraries} +As with previous work to extend formal languages with security, in order to formalize this framework, one needs +to produce a form of component library that represents the possible combinations, or solutions, that a designer +or developer can pull from to generate new implementation models. Listing~\ref{lst:AADLUserDefineLow}) shows an example of how one could use AADL to define properties on a processor. +% Add in the table of elements and variations +\begin{table*}[] +\centering +\caption{Table illustrating different component variations} +\label{elementTypes} +\begin{tabular}{@{}llllll@{}} +\toprule +\multicolumn{6}{c}{Component Types Table} \\ \midrule +\multicolumn{1}{c}{\multirow{2}{*}{{\underline{\textbf{Elements}}}}} & \multicolumn{5}{c}{\textbf{Types}} \\ +\multicolumn{1}{c}{} & \multicolumn{1}{c}{{\underline{\textbf{I}}}} & \multicolumn{1}{c}{{\underline{ \textbf{II}}}} & \multicolumn{1}{c}{{\underline{\textbf{III}}}} & \multicolumn{1}{c}{{\underline{\textbf{IV}}}} & \multicolumn{1}{c}{{\underline{ \textbf{V}}}} \\ +Memory & Unprotected & Protected & Encrypted & Obfuscated & Combo \\ +Bus & Unprotected & Encrypted & Non-sniffable & & \\ +Processor & Simple & Embedded Encryption & Pure Encryption & & \\ +Data & Plain-text & Encryption & Protected & & \\ +Port & Normal & Encrypted & Protected & & \\ \bottomrule +\end{tabular} +\end{table*} + +As shown in Table~\ref{elementTypes}, this paper has defined potential component types that would populate the architectural space of this new security framework. To show how these component elements would define a larger design, this paper moves to define and describe a `system' in this new framework. A system is defined as a grouping of elements that serve a given purpose. This grouping is created via the combination of different circuit elements to perform a specific task or function. Furthermore, this new system can be abstracted into a `single layer' device object model. + +It should be noted that variations come from a mixture of different element groupings that come together to form one larger system element; due to the nature of a system there is a lot more granularity that can be used to express the properties of said system element. A regular or simple system has no encryption, no data access control, no assurance of ``security level maintained''. In this implementation one can interpret everything is at the ``default'' lowest level of ``security'' that can be assured. An encrypted system has at least encryption implemented to some degree. It could be encryption on the input or output, bus, memory or processor. Any mixture of the aforementioned `levels' of encryption is possible, but must be verifiable; due to the need of verifying security. A protected system contains elements that either interact or are responsible for access control to ``secure'' data, information, or services. + \begin{lstlisting}[caption={Example of User-defined Lower Level Components},label={lst:AADLUserDefineLow}] system implementation transmitter.encrypt_i -- Subcomponents of the transmitter @@ -350,6 +375,21 @@ processor implementation procbase.encryptembedded_i end procbase.encryptembedded_i; \end{lstlisting} +\subsection{Security Requirements} +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. 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. +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. 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 +be met by a given implementation. + + \begin{lstlisting}[caption={User-defined Higher Level Security Requirement},label={lst:AADLUserDefineHigh}] abstract implementation sysreq.wireless_sensor_i subcomponents @@ -374,40 +414,22 @@ abstract implementation sysreq.wireless_sensor_i end sysreq.wireless_sensor_i; \end{lstlisting} -%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. 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. Otherwise the advantages of this new security framework would not outweigh the cost and time spend learning the syntax and tools required. +\subsection{Mapping Tools} -% Add in the table of elements and variations -\begin{table*}[] -\centering -\caption{Table illustrating different component variations} -\label{elementTypes} -\begin{tabular}{@{}llllll@{}} -\toprule -\multicolumn{6}{c}{Component Types Table} \\ \midrule -\multicolumn{1}{c}{\multirow{2}{*}{{\underline{\textbf{Elements}}}}} & \multicolumn{5}{c}{\textbf{Types}} \\ -\multicolumn{1}{c}{} & \multicolumn{1}{c}{{\underline{\textbf{I}}}} & \multicolumn{1}{c}{{\underline{ \textbf{II}}}} & \multicolumn{1}{c}{{\underline{\textbf{III}}}} & \multicolumn{1}{c}{{\underline{\textbf{IV}}}} & \multicolumn{1}{c}{{\underline{ \textbf{V}}}} \\ -Memory & Unprotected & Protected & Encrypted & Obfuscated & Combo \\ -Bus & Unprotected & Encrypted & Non-sniffable & & \\ -Processor & Simple & Embedded Encryption & Pure Encryption & & \\ -Data & Plain-text & Encryption & Protected & & \\ -Port & Normal & Encrypted & Protected & & \\ \bottomrule -\end{tabular} -\end{table*} +%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. -As shown in Table~\ref{elementTypes}, this paper has defined potential component types that would populate the architectural space of this new security framework. To show how these component elements would define a larger design, this paper moves to define and describe a `system' in this new framework. A system is defined as a grouping of elements that serve a given purpose. This grouping is created via the combination of different circuit elements to perform a specific task or function. Further more, this new system can be abstracted into a `single layer' device object model. -It should be noted that variations come from a mixture of different element groupings that come together to form one larger system element; due to the nature of a system there is a lot more granularity that can be used to express the properties of said system element. A regular or simple system has no encryption, no data access control, no assurance of ``security level maintained''. In this implementation one can interpret everything is at the ``default'' lowest level of ``security'' that can be assured. An encrypted system has at least encryption implemented to some degree. It could be encryption on the input or output, bus, memory or processor. Any mixture of the aforementioned `levels' of encryption is possible, but must be verifiable; due to the need of verifying security. A protected system contains elements that either interact or are responsible for access control to ``secure'' data, information, or services. +\subsection{Verification Tools} + 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. Otherwise the advantages of this new security framework would not outweigh the cost and time spend learning the syntax and tools required. -As with previous work to extend formal languages with security, in order to formalize this framework, one needs to produce a form of component library that represents the possible combinations, or solutions, that a designer or developer can pull from to generate new implementation models. Once separate libraries of components and potential security requirements had 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. 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. 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 be met by a given implementation. - -Thanks to the extensibility of the AADL language, coupled with the powerful annexes and tools that the user-community has developed and refined, it is the aim of this paper to produce a new and flexible security framework. This new framework will allow for AADL to specify security requirements while expanding the existing lexicon to define component properties and capabilities. The advantage of using the AADL language is that the framework can be further augmented through existing annexes and tools. % Mention how exploration of the entire design space is paramount to effective use of the framework; hence without a form of automation this tool can not be adequately used to generate secure model implemenations based on requirements and specifications. \section{Conclusion} \label{Conclusion} -With the use of the proposed security framework, designers and developers would have an effective and efficient manner by which security implementations and models can be verified and validated, allowing for visibility in the early phase design process and ideally saving time. Defining, formally describing, and validation of security needs and requirements is paramount to the future design and development of real-time embedded systems, especially with the growth of the Internet-of-Things (IoT) devices. There is a need for methods and tools that will allow for exploration of the entire design space. Further automation of such tools is the most efficient manner for generating secure model implementations based on requirements and specifications. Future work includes: formulation of a mapping process to take security requirements and component specifications as input and output model implementations that can be verified and validated. Verification tools for validating generated model implementations need to be developed. Lastly, augmenting this paper's efforts towards creating a better security framework by coupling the use of existing AADL annexes and tools (e.g. BLESS and EMV2) to allow for modeling of security behavior. Ultimately, this paper believes that AADL, its extensive user-community, and inherent extensibility make it the best linguistic tool to achieve the goal of a formalized, effective, security framework for design model generation and verification. +Thanks to the extensibility of the AADL language, coupled with the powerful annexes and tools that the user-community has developed and refined, it is the aim of this paper to produce a new and flexible security framework. This new framework will allow for AADL to specify security requirements while expanding the existing lexicon to define component properties and capabilities. The advantage of using the AADL language is that the framework can be further augmented through existing annexes and tools. +With the use of the proposed security extensions to AADL, designers and developers would have an effective and efficient manner by which security implementations and models can be verified and validated, allowing for visibility in the early phase design process and ideally saving time. Defining, formally describing, and validation of security needs and requirements is paramount to the future design and development of real-time embedded systems, especially with the growth of the Internet-of-Things (IoT) devices. There is a need for methods and tools that will allow for exploration of the entire design space. Further automation of such tools is the most efficient manner for generating secure model implementations based on requirements and specifications. Future work includes: formulation of a mapping process to take security requirements and component specifications as input and output model implementations that can be verified and validated. Verification tools for validating generated model implementations need to be developed. Lastly, augmenting this paper's efforts towards creating a better security framework by coupling the use of existing AADL annexes and tools (e.g. BLESS and EMV2) to allow for modeling of security behavior. Ultimately, this paper believes that AADL, its extensive user-community, and inherent extensibility make it the best linguistic tool to achieve the goal of a formalized, effective, security framework for design model generation and verification. % % ---- Bibliography ----