From a1fab11cfd41f2753f3a4e5e5d1410349f363b57 Mon Sep 17 00:00:00 2001 From: Duncan Date: Fri, 10 Jun 2016 09:36:25 -0400 Subject: [PATCH] Addition of examples from CODES paper. Ask Chandy about which listings make sense as an example --- AADLSecPaper.tex | 61 ++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 59 insertions(+), 2 deletions(-) diff --git a/AADLSecPaper.tex b/AADLSecPaper.tex index 7c22438..8ca37fd 100644 --- a/AADLSecPaper.tex +++ b/AADLSecPaper.tex @@ -309,13 +309,70 @@ \section{Proposed Extensions to AADL} 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:AADLSecEncryption}) - \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:AADLSecLevels}) + \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 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}. + +\begin{lstlisting}[caption={Example of User-defined Lower Level Components},label={lst:AADLUserDefineLow}] +system implementation transmitter.encrypt_i + -- Subcomponents of the transmitter + subcomponents + ant_in : system recv_antenna.normal_i; + ant_out : system trns_antenna.encrypt_i; + encrproc : processor procbase.encryptembedded_i; + -- Connection definitions of the transmitter + connections + c0 : port ant_in.wired_out -> encrproc.input_port; + c1 : port encrproc.output_port -> ant_out.wired_in; + -- Flow path definition for the transmitter + flows + f0 : end to end flow ant_in.f0 -> c0 -> encrproc -> c1 -> ant_out.f0; + -- Additional properties of the transmitter + properties + securityspecs::has_encryption => true; +end transmitter.encrypt_i; + +processor implementation procbase.encryptembedded_i + properties + securityspecs::has_encryption => true; + securityspecs::encryptmodule_class => embedded; + securityspecs::encryption_class => AES; + securityspecs::encryption_variation => b256; + securityspecs::has_PUF => false; + securityspecs::has_TPM => false; + securityspecs::has_encryptedflash => false; + securityspecs::isTamperProof => false; +end procbase.encryptembedded_i; +\end{lstlisting} + +\begin{lstlisting}[caption={User-defined Higher Level Security Requirement},label={lst:AADLUserDefineHigh}] +abstract implementation sysreq.wireless_sensor_i + subcomponents + serv_ADConv: abstract sysserv.ADConv_i { + servatrb::dynamicRange => 0..5 V; + secatrb::integrity::atkImpact => 300; + }; + serv_wrlsTrans: abstract sysserv.wrlsTrans_i { + servatrb::distance => 100 m; + secatrb::authentication::atkValue => 600; + secatrb::authentication::atkImpact => 400; + secatrb::authorization::atkImpact => 1200; + secatrb::dataleakage::atkImpact: => 800; + secatrb::dataleakage::atkValue: => 800; + }; + fnc_data: abstract security_props.data_i { + dataatrb::data_class => Sensor; + secatrb::atkImpact => 800; + properties + secatrb::hasProtection => false; + secatrb::AuthGroup => Employees; +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.