Deletions and edits to RDAL, BLESS, and EMV2 sections

AADLSecPaper.tex

@@ -201,7 +201,7 @@ Resolute is a language and tool for developing architectural assurance cases~\ci
 %	\label{fig:AADLResoluteExample}
 %\end{figure}
 
-The Requirements Definition and Analysis Language Tool Environment (RDALTE) is a requirements modeling and validation tool for AADL.  This tool allows for organizing requirements and assumptions into packages~\cite{RDALOverview}.  This allows for users to group dependent requirements into common packages.  RDALTE helps to separate concerns between the requirements and the constraints of a system, while also detailing a clear identification between assumptions and requirements.  As with the Resolute tool, RDALTE allows for effective implementation and verification of system requirement definition and analysis but is not primarily focused on security requirements or constraints.  Though, as with all extensions and plug-in of AADL, it is possible for a user to expand on the existing tool to be able to handle security needs.  RDALTE would allow for constructive overlap of security requirements with the Resolute tool, while the constraint definition aspect can be used for describing both the component and security constraints that an embedded systems model must maintain.
+The Requirements Definition and Analysis Language Tool Environment (RDALTE) is a requirements modeling and validation tool for AADL.  This tool allows for organizing requirements and assumptions into packages~\cite{RDALOverview}; allowing for users to group dependent requirements into common packages.  RDALTE helps to separate concerns between the requirements and the constraints of a system, while also detailing a clear identification between assumptions and requirements.  RDALTE would allow for constructive overlap of security requirements with the Resolute tool, while the constraint definition aspect can be used for describing both the component and security constraints that an embedded systems model must maintain.
 
 The Error-Model Annex is purposed with tracking errors and their propagation throughout a system.  The annex can also be used to describe component error behavior as transitions between different states, where transitions are triggered by error events and incoming propagations of error from other parts of the system design.  The annex declarations allow for the definition of~\cite{EMV1}:
 \begin{enumerate}
@@ -212,15 +212,16 @@ The Error-Model Annex is purposed with tracking errors and their propagation thr
 	\item Component error behavior.
 	\item Composite error behavior.
 \end{enumerate}
-The extended linguistics of describing these facets are defined with the error model library.  As with all other aspects of AADL, this error model library can also be user extended to allow for new error types or even an extension of the error type hierarchy.  In current examples~\cite{Osate2Examples} this annex is noted as `EMV2'.  This is due to the development of the error-modeling annex to allow for both the original error-model annex and version 2 to co-exist~\cite{EMV2}.  The advantage of this tool development is that a user can now define not only the architectural specifications of a design but also that systems behavior under unknown or unexpected conditions.  Since AADL is originally focused on the architectural definition of modeled systems, the propagation paths of the error-modeling annex are determined by the architecture.  From a security standpoint this is advantageous because this allows developers to flag unexpected behavior or states that an attack might be able to take advantage of.  From a developer's standpoint, the advantage is that in the early design phases not all actions or behavior may have been thoroughly documented or even planned out.  This annex would allow for planning on possible behavioral complications that would produce errors or cause a system to no longer function correctly.  For example, how should a modeled security system behave if a client does not have any of the encryption or authentication methods that a server relies on to maintain a secure and protected connection.  While not purposed for security error-behavior, the tools can be improved to allow for the tracking of odd or unexpected security behavior that can be know from an early design phase.  The disadvantage of this being that while the error behavior can be modeled and verified, the security behavior of the system, and its components, is not readily tracked by this same tool and would require time and effort to implement and improve the language in a standardized manner.
+The extended linguistics of describing these facets are defined with the error model library.  From a security standpoint this is advantageous because this allows developers to flag unexpected behavior or states that an attack might be able to take advantage of.  From a developer's standpoint, the advantage is that in the early design phases not all actions or behavior may have been thoroughly documented or even planned out.  While not purposed for security error-behavior, the tools can be improved to allow for the tracking of odd or unexpected security behavior that can be know from an early design phase.  
+The disadvantage of this being that while the error behavior can be modeled and verified, the security behavior of the system, and its components, is not readily tracked by this same tool and would require time and effort to implement and improve the language in a standardized manner.
 
-Behavior Language for Embedded Systems with Software (BLESS) is a formal specification and verification tool purposed with formalizing the semantics of the existing Behavioral Annex (BA) sublanguage~\cite{BLESS2013}.  If one defines AADL as a purely structure based language, BLESS is the user-community writing a language that is purely focused on behavior.  In fact, BLESS programs are attached to system architectures to define component behavior because the community felt that AADL lacked a formal behavior interface specification language, needed a formal component behavior language, and required a set of verification methods and tools to ensure compliance of behavior implementation meeting specifications of the model.  The BLESS language works to mathematically define embedded programs, their specifications, and their executions from~\cite{BLESS2013}:
+Behavior Language for Embedded Systems with Software (BLESS) is a formal specification and verification tool purposed with formalizing the semantics of the existing Behavioral Annex (BA) sublanguage~\cite{BLESS2013}.  If one defines AADL as a purely structure based language, BLESS is the user-community writing a language that is purely focused on behavior.  The BLESS language works to mathematically define embedded programs, their specifications, and their executions from~\cite{BLESS2013}:
 \begin{enumerate}
 	\item assertions to provide a formal behavior interface specification language.
 	\item annex subclauses for providing a formal component behavior language.
 	\item provide a proof tool that enables user of verification methods to show that model implementations meet defined system specifications with auditable evidence of compliance of the behaviors to specification.
 \end{enumerate}
-The act of proving that the system behavior and execution upholds defined specifications is done through the use of contracts defined for AADL component interfaces, descriptions of the internal component behaviors, and the annotation of programs using BLESS assertions to form `proof outlines'.  These outlines can then be transformed, through the use of the proof tool, into proofs.  BLESS was very much inspired by BA~\cite{BLESS2013}, and as such BLESS works to standardized not only the language but the process through the use of state-transition systems coupled with simple temporal logic formulas.  To aid in BLESS' adoptability verification conditions are representation as a Hoare triple, allowing for use with other formal verification techniques.  It is worth noting that while BLESS' proof tool will verify conditions generated through AADL and check existing proofs, it is by not means a tool for proving theorems.  In other words, the tool depends on the knowledge of the user and assumes that the proofs provided to the BLESS tool are inherently correct.  Current work on development and improvement of the tool include working towards augmenting BLESS behavioral models with EMV2 error models along with adding simulation and code generation to the list of capabilities.  From a security viewpoint, this tool allows for a more complete description and verification of component and system behavior.  With additional extension, BLESS can be tailored to allow for the tacking and proof-checking of security-centric behavior and execution of defined models.  For example, mapping the behavior of authentication and authorization elements.  In these cases a designer will need to define behavior for unexpected attempt to authorize or authenticate access rights.  This behavior definition would then need to be definable as a set of Hoare triples for formal verification of secure system behavior.  The next step is developing a method for converting requirements and component definitions into a Hoare triple type notation for use with known formal verification methods.  This would greatly aid in making AADL a standard for security behavior and requirement specification design.  Coupling this work with the EMV2 AADL extension, a user could not only define the expected behavior and correctness of secure component execution, but also model the unexpected or strange behavior that an attacker would rely on for attacking a system.  This combination of efforts would allow for a far better modeling and mapping of the entire system behavior under secure conditions.  Unfortunately, BLESS is not focused on security behavior modeling and does not have the language necessary to begin describing security requirements of behavior.
+The act of proving that the system behavior and execution upholds defined specifications is done through the use of contracts defined for AADL component interfaces, descriptions of the internal component behaviors, and the annotation of programs using BLESS assertions to form `proof outlines'.  These outlines can then be transformed, through the use of the proof tool, into proofs.  BLESS was very much inspired by BA~\cite{BLESS2013}, and as such BLESS works to standardized not only the language but the process through the use of state-transition systems coupled with simple temporal logic formulas.  To aid in BLESS' adoptability verification conditions are representation as a Hoare triple, allowing for use with other formal verification techniques.  It is worth noting that the tool depends on the knowledge of the user and assumes that the proofs provided to the BLESS tool are inherently correct.  With additional extension, BLESS can be tailored to allow for the tacking and proof-checking of security-centric behavior and execution of defined models.  For example, mapping the behavior of authentication and authorization elements.  In these cases a designer will need to define behavior for unexpected attempt to authorize or authenticate access rights.  This behavior definition would then need to be definable as a set of Hoare triples for formal verification of secure system behavior.  Coupling this work with the EMV2 AADL extension, a user could not only define the expected behavior and correctness of secure component execution, but also model the unexpected or strange behavior that an attacker would rely on for attacking a system.  Unfortunately, BLESS is not focused on security behavior modeling and does not have the language necessary to begin describing security requirements of behavior.
 
 \subsection{AADL Security Annex Limitations}
 Overall, the limitations of the current AADL security annex and analysis tools are that there is no focus on defining