Additional writing to Limitations section and Proposed AADL section

AADLSecPaper.tex

@@ -223,6 +223,12 @@ Behavior Language for Embedded Systems with Software (BLESS) is a formal specifi
 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.
 
 \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 
+the security requirements and component specifications are restrained to vaguely defined terms about exposure and 
+functional language.  This does not allow for effective description of the behavior and security constraints of these modeled
+systems.  Neither does the prevailing lexicon examine the capabilities of the described components or grant the ability to thoroughly
+explore the design space while maintaining assurances based on user-defined security constraints.
+
 Taking a deeper look at these developments for the AADL language, there are certain improvements that this paper 
 believes are a step in the right direction.  Including a numerical value to `security levels' allows for 
 quantitative analysis of this property through a system's design.  The concept of exposure (e.g. how exposed a 
@@ -334,9 +340,9 @@ As shown in Table~\ref{elementTypes}, this paper has defined potential component
 
 It should be noted that variations come from a mixture of different element groupings that come together to form one larger system element; due to the nature of a system there is a lot more granularity that can be used to express the properties of said system element.  A regular or simple system has no encryption, no data access control, no assurance of ``security level maintained''.  In this implementation one can interpret everything is at the ``default'' lowest level of ``security'' that can be assured.  An encrypted system has at least encryption implemented to some degree.  It could be encryption on the input or output, bus, memory or processor.  Any mixture of the aforementioned `levels' of encryption is possible, but must be verifiable; due to the need of verifying security.  A protected system contains elements that either interact or are responsible for access control to ``secure'' data, information, or services.
 
-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.  Once separate libraries of components and potential security requirements had 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.  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.
+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.  Once separate libraries of components and potential security requirements had 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.  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 represent the core elements being protected, how these components must be protected, and the standards that must be met by a given implementation.
 
-Thanks to the extensibility of the AADL language, coupled with the powerful annexes and tools that the user-community has developed and refined, it is the aim of this paper to produce a new and flexible security framework.  The advantage of using the AADL language is that the framework can be further augmented through existing annexes and tools.  
+Thanks to the extensibility of the AADL language, coupled with the powerful annexes and tools that the user-community has developed and refined, it is the aim of this paper to produce a new and flexible security framework.  This new framework will allow for AADL to specify security requirements while expanding the existing lexicon to define component properties and capabilities.  The advantage of using the AADL language is that the framework can be further augmented through existing annexes and tools.  
 
 % Mention how exploration of the entire design space is paramount to effective use of the framework; hence without a form of automation this tool can not be adequately used to generate secure model implemenations based on requirements and specifications.