Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
Addition of examples from CODES paper. Ask Chandy about which listing…
…s make sense as an example
  • Loading branch information
Duncan committed Jun 10, 2016
1 parent 4f35f8c commit a1fab11
Showing 1 changed file with 59 additions and 2 deletions.
61 changes: 59 additions & 2 deletions AADLSecPaper.tex
Expand Up @@ -309,13 +309,70 @@ 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: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.

Expand Down

0 comments on commit a1fab11

Please sign in to comment.