More paper edits to Section 4. Added Resolute example and additional …

…writing to Mapping Tools subsection. Added some notes to 4.2 about ALISA, but need to remove more writing to add more than a one sentence reference to the ALISA work.

AADLSecPaper.tex

@@ -382,13 +382,13 @@ 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.  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. 
+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. 
 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 
+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 
 be met by a given implementation.
 
@@ -420,11 +420,27 @@ end sysreq.wireless_sensor_i;
 \subsection{Mapping Tools}
 
 %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 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.
+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.
+
+\begin{lstlisting}[caption={User-defined Resolute Checks},label={lst:AADLUserDefineResolute}]
+package arch_resolute_checks
+public
+
+annex resolute {**
+check_encryption_flow(comp : component) <=
+    ** " Check the encryption property of connections of features on component " comp **
+    forall (conn : connections(comp)) . has_property(source(conn), securityspecs::has_encryption) and
+        has_property(destination(conn), securityspecs::has_encryption) => 
+        (property(source(conn), securityspecs::has_encryption)) = (property(destination(conn), securityspecs::has_encryption))
+**};
+
+end arch_resolute_checks;
+\end{lstlisting}
+
 Further work is needed 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.  
 
 
@@ -660,6 +676,11 @@ Sangiovanni-Vincentelli, A.:
 Quo vadis, SLD? Reasoning about the trends and challenges of system level design,
 Proceedings of the IEEE, Volume 95 Number 3, pages 467--506 (2007)
 
+\bibitem {ALISA2016}
+Delange, J., Feiler, P., Neil, E.:
+Incremental Life Cycle Assurance of Safety-Critical Systems,
+8th European Congress on Embedded Real Time Software and Systems (ERTS 2016)
+
 \end{thebibliography}
 
 \end{document}