Simple edits to the paper. Next push to be potential areas to remove;…

… could help with allowing for a little more writing on ALISA.

AADLSecPaper.tex

@@ -112,7 +112,7 @@ This paper is organized as follows: Section ~\ref{Motivation and Related Work} p
 
 \section{Motivation and Related Work}
 \label{Motivation and Related Work}
-Over the past few decades there have been research towards defining security in a formalized and verifiable manner.  The work has ranged from determining the security requirements of a system to standardizing formal implementation and methods of verification for produced models.  The movement of security concerns from a server-like systems to more embedded system architectures has lead to new constraints and considerations that must be accounted for.  Further more, as mentioned in Section ~\ref{securityBasics}, as security requirements and implementations change over time the schema for security model generation and verification needs to adapt.
+Over the past few decades there have been research towards defining security in a formalized and verifiable manner.  The work has ranged from determining the security requirements of a system to standardizing formal implementation and methods of verification for produced models.  The movement of security concerns from server-like systems to more embedded system architectures has lead to new constraints and considerations that must be accounted for.  Further more, as mentioned in Section ~\ref{securityBasics}, as security requirements and implementations change over time the schema for security model generation and verification needs to adapt.
 
 Previous work in defining security requirements range from lesser known languages, such as i* and SI*, to more commonly used one, such as UMLSec and SysML-Sec.  Markose et.~al.~propose an object oriented methodology for structuring security requirements analysis methodology~\cite{markose2008systematic}.  This work focused on deriving requirements based on security use cases at different levels of system hierarchy.  The advantage being that aggregation of the derived security requirements represents the security requirement specification for the entire system.  Other languages that focus on specifying security requirements are `i*'~\cite{yu1997towards} and `SI*'~\cite{massacci2010security}.  The work by Eric Yu~\cite{yu1997towards} aimed to replace the current standard modeling and reasoning support used for determining early phase requirements engineering.  Although the purpose for this work was about organizational environments and their information systems, the `i*' framework applies to business process modeling and redesign, software process modeling, and modeling of embedded systems.  Massacci et.~al.'s work with `SI*' showed not only the effectiveness of agent-oriented methodologies but also was revised and refined to be applicable in the earliest phases of software development processes and cover a broader organizational perspective.
 
@@ -136,7 +136,7 @@ The Architecture Analysis \& Design Language (AADL) is traditionally design for
 	\item Modeling of large-scale systems.  Modeling is done through the use of component variants, layered system modeling, packaging, abstraction, prototyping, parameterized templates, arrays of components, and connection patterns.
 	\item Accommodation of diverse analysis needs.  This is managed through extension mechanisms for the language along with standardization of said extensions.
 \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.
+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-defined 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.
 
@@ -191,7 +191,7 @@ More current work on the development of a security annex for AADL has been relea
 \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}.  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.  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
@@ -284,7 +284,7 @@ supported_operations_mode         :
 %	\label{fig:AADLSecEncryption}
 %\end{figure}
 
-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:
+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:
 \begin{enumerate}
 	\item Does the key generated 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?
@@ -323,7 +323,7 @@ Other additional aspects of this framework, that could come from the existing to
 \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 and an encrypted transmitter.
+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 and an encrypted transmitter.
 % Add in the table of elements and variations
 \begin{table*}[]
 \centering
@@ -424,7 +424,7 @@ As can be seen in Figure~\ref{fig:AADLSecFrame} the power of this new framework
 
 
 \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}; an example of examining that all connections between given components maintain an expectation of encryption.  In other words, the Resolute check ensures that data expected to pass between multiple components remains encrypted throughout the entire component definition.
+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.
 
 \begin{lstlisting}[caption={User-defined Resolute Checks},label={lst:AADLUserDefineResolute}]
 package arch_resolute_checks
@@ -647,7 +647,7 @@ Proceedings of the 25th edition on Great Lakes Symposium on VLSI, pages 15--20 (
 Common Criteria for Information Technology Security Evaluation,
 ISO/IEC, Number ISO/IEC 15408, July 2015
 
-\bibitem {benzel2005design},
+\bibitem {benzel2005design}
 Benzel, T.V., Irvine, C.E., Levin, T.E., Bhaskara, G., Nguyen, T.D., Clark, P.C.:
 Design principles for security (2005)