Permalink
Cannot retrieve contributors at this time
Name already in use
A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
AADLPaper_SSR/AADLSecPaper.tex
Go to fileThis commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
694 lines (578 sloc)
64.5 KB
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| % This is based on the LLNCS.DEM the demonstration file of | |
| % the LaTeX macro package from Springer-Verlag | |
| % for Lecture Notes in Computer Science, | |
| % version 2.4 for LaTeX2e as of 16. April 2010 | |
| % | |
| % See http://www.springer.com/computer/lncs/lncs+authors?SGWID=0-40209-0-0-0 | |
| % for the full guidelines. | |
| % | |
| \documentclass{llncs} | |
| % Table package needs | |
| \usepackage{tabularx,booktabs} | |
| \usepackage{multirow} | |
| \usepackage[normalem]{ulem} | |
| \usepackage[english]{babel} | |
| % Image package needs | |
| \usepackage{graphicx} | |
| %\usepackage{graphics} | |
| \usepackage{listings} % Include the listings-package | |
| \usepackage{color} | |
| \usepackage{balance} | |
| \useunder{\uline}{\ul}{} | |
| \definecolor{darkgreen}{rgb}{0,0.5,0} | |
| \definecolor{mygreen}{rgb}{0,0.6,0} | |
| \definecolor{mygray}{rgb}{0.5,0.5,0.5} | |
| \definecolor{mymauve}{rgb}{0.58,0,0.82} | |
| \lstset{ % | |
| backgroundcolor=\color{white}, % choose the background color; you must add \usepackage{color} or \usepackage{xcolor} | |
| basicstyle=\ttfamily\scriptsize, % the size of the fonts that are used for the code | |
| breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace | |
| breaklines=true, % sets automatic line breaking | |
| captionpos=b, % sets the caption-position to bottom | |
| commentstyle=\color{mygreen}, % comment style | |
| deletekeywords={...}, % if you want to delete keywords from the given language | |
| escapeinside={\%*}{*)}, % if you want to add LaTeX within your code | |
| extendedchars=true, % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8 | |
| frame=single, % adds a frame around the code | |
| keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible) | |
| keywordstyle=\color{blue}, % keyword style | |
| % language=C, % the language of the code | |
| morecomment=[l]{--}, | |
| morekeywords={property,set,is,type, constant, enumeration, end, applies, to, inherit, of, *,...}, % if you want to add more keywords to the set | |
| numbers=left, % where to put the line-numbers; possible values are (none, left, right) | |
| numbersep=5pt, % how far the line-numbers are from the code | |
| numberstyle=\tiny\color{mygray}, % the style that is used for the line-numbers | |
| rulecolor=\color{black}, % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here)) | |
| showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces' | |
| showstringspaces=false, % underline spaces within strings only | |
| showtabs=false, % show tabs within strings adding particular underscores | |
| stepnumber=1, % the step between two line-numbers. If it's 1, each line will be numbered | |
| stringstyle=\color{mymauve}, % string literal style | |
| tabsize=2, % sets default tabsize to 2 spaces | |
| title=\lstname % show the filename of files included with \lstinputlisting; also try caption instead of title | |
| } | |
| \begin{document} | |
| \title{AADL Language Review and Expansion with Respect to Security Behavior and Requirements} | |
| % | |
| \titlerunning{AADL Security} % abbreviated title (for running head) | |
| % also used for the TOC unless | |
| % \toctitle is used | |
| % | |
| %\author{Paul Wortman \and John A. Chandy} | |
| % | |
| %\authorrunning{Ivar Ekeland et al.} % abbreviated author list (for running head) | |
| % | |
| %%%% list of authors for the TOC (use if author list has to be modified) | |
| %\tocauthor{Ivar Ekeland, Roger Temam, Jeffrey Dean, David Grove, | |
| %Craig Chambers, Kim B. Bruce, and Elisa Bertino} | |
| % | |
| %\institute{University of Connecticut, Storrs CT 06269, USA}%\\ | |
| %\email{I.Ekeland@princeton.edu},\\ WWW home page: | |
| %\texttt{http://users/\homedir iekeland/web/welcome.html} | |
| %\and | |
| %Universit\'{e} de Paris-Sud, | |
| %Laboratoire d'Analyse Num\'{e}rique, B\^{a}timent 425,\\ | |
| %F-91405 Orsay Cedex, France} | |
| \maketitle % typeset the title of the contribution | |
| \begin{abstract} | |
| AADL is a common use language that has been developed and tweaked over the years to allow the ability to | |
| describe model behavior and specifications, with more recent attempts to define language for security | |
| requirements and verification. This paper examines previous implementations of behavior, requirements, and | |
| security in AADL and then goes to propose a new framework for better integration and description of security | |
| requirements and behavior within the AADL lexicon. | |
| \keywords{security modeling, security framework, secure system design} | |
| \end{abstract} | |
| \section{Introduction} | |
| The Architecture Analysis \& Design Language (AADL) is an architecture description language standardized by the Society of Automotive Engineers (SAE). AADL is purposed to capture system architectures with design requirements, validating that architecture, and performing early analysis to detect errors and other issues to avoid late re-engineering efforts. AADL contains constructs for modeling both software and hardware components; hardware components named as ``execution platform'' components within the standard. The produced architecture models can then be used either as a design documentation, for analysis or for code generation. System and software architecture is defined through the use of specialized components with interfaces and the description of the interaction of these components with the execution environment (e.g. processor, buses). This functionality can be further extended through different mechanisms; user-defined properties for integrating customized constraints or existing AADL Annexes. | |
| Recent work on extending AADL's capabilities and tools has ranged from the development of error tracking, behavioral descriptions and definitions, code generation, requirement modeling, security description and definition, as well as verification of proposed system models and implementations. With such research and effort being poured into the many facets of the language, AADL is becoming a more powerful and well rounded tool. Due to the ease by which new extensions and user-define additions can be created for AADL, the community is greatly responsible for the development and improvement of AADL as a modeling and analysis tool. More on these annexes and extensions will be examined in Section ~\ref{AADL Annexes and Extensions} along with their affect on the overall use and growth on the tools use and potential. | |
| \label{securityBasics} | |
| Secure systems design is a formidable and troublesome obstacle that is not well understood and even more poorly implemented. From examples of Jeep Cherokee's security weaknesses~\cite{jeepHack}, airplane hacker scares~\cite{planeHack}, adware implementation weaknesses~\cite{superFish}\cite{lenovoWPBT}, government employee data breaches~\cite{govHack}, code implementation concerns~\cite{stageFright}, and other update security | |
| concerns~\cite{androidMarshmallow,googleAndroid} one can see that a lack of standardized security design and implementation can render catastrophic failure. This issue is further exacerbated by how vast the problem space is (e.g. secure software, trusted platform modules, new authentication methods)~\cite{aaraj2008analysis,denning1996location,%mapayi2013evaluating, lin2015security, shi2013new, son2015software, | |
| saito2015case,denning2015toward,nguyen2015model,ravi2004security,gokhale2008model,perez2006vtpm,yan2015novel,tehranipoor2015dram}. | |
| Security is always evolving as knowledge | |
| of encryption techniques, authentication technologies, access control methods and other security mechanisms change over | |
| time. From a system design standpoint, one has to balance security needs with traditional system design properties. | |
| % Similarly tolerance, chip capabilities, power distribution of hardware design, signal lag and crosstalk are important in terms of hardware considerations. | |
| %The primary cost of incorporating security into the design process and actually operating a secure system is time. There are the monetary and hardware costs of security development and implementation, but even those aspects all have a time cost coupled with them. | |
| A lack of formal definition of standards lends to the heavy time cost of designing and implementing a security framework. One needs to settle on an effective methodology that has enough rigidity to act as a standard, but still maintains a degree of flexibility to allow for further expansion and future development. Security must be paramount in design from the very beginning of any development cycle. | |
| Security has many facets to it: failure, processes, security mechanisms, security principles, security policies, trust, etc. Security vulnerabilities are mainly due to incorrect implementations or incorrect assumptions about functionality, both of which are easily avoided by rigorous planning and design. Further complications can arise when implementing different concepts and methods for creating layers of security. The key aspects to simplifying this daunting field are standardization of encryption algorithms, authentication methods and communication protocols. Work made towards this goal include a framework for the derivation of system requirements by the Common Criteria standard~\cite{CommonCriteria}, review and analysis of fundamental security principles over more than four decades of research and development in information security technology~\cite{benzel2005design}, and work to include security into systems that had not been designed for security~\cite{lin2013security}. While there are existing tools for the validation and verification of existing security models (e.g. Resolute for AADL), there is a severe lack of tools to generate security models. | |
| This paper is organized as follows: Section ~\ref{Motivation and Related Work} presents the related work in security with other languages and the motivation for focusing on AADL. Section ~\ref{AADL Annexes and Extensions} examines the current tool and annex extensions for AADL as well as the more recent inclusions of security definitions and descriptions. Section ~\ref{New Framework} presents this paper's work to create a new security framework for model generation and verification. Section ~\ref{Conclusion} summarizes the work on this paper and presents future work for developing the proposed framework. | |
| \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 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. | |
| %Section on UMLSec. | |
| UMLSec is an extension to the Unified Modeling Language (UML) for integrating security related information using UML specifications. UMLSec is centered around secure systems development using specification elements to present recurring security requirements such as secrecy, integrity, and authenticity~\cite{jurjens2005secure}. The reasoning for J\"{urjens} to use the Unified Modeling Language (UML) was due to it being a de facto standard in industrial modeling with a large number of developers trained in its use~\cite{jurjens2002umlsec}. Compared to previous notations and languages with similar user community sizes, UML was relatively precisely defined making it a prime candidate. As a lightweight extension for UML, the UMLSec profiles are defined between the system being modeled and an attacker model that defines the threats posed. The limitation of this work is that the focus on security requirements is from a networking scope. While this is effective from a larger industrial standpoint, this implementation does not account for lower level component security requirements or behavior. | |
| %Section on SysML-Sec | |
| SysML-Sec is an environment tool used to design safe and secure embedded systems as an extension of the Systems Modeling Language(SysML) which is a dialect of the Unified Modeling Language (UML)~\cite{SysML-Sec}. SysML-Sec focuses on both the software and the hardware of the modeled systems. The originating language, SysML, is a general purpose visual modeling language purposed for system engineering applications~\cite{SysML}. SysML is defined as a dialect of the UML standard that is able to support the specification, analysis, design, verification, and validation of not only systems but also systems-of-systems. The nature of SysML-Sec, extending from such well established standard languages, allows for security-aware system architecture definition and exploration along with the definition of attack graphs. This allows for similar description to the `attacker model' that can be created using UMLSec. While a powerful tool that includes views from both a system and attacker standpoint, there is still too much of a focus on the impact of security mechanisms over the safety and performance of the overall system to meet our needs of defining security requirements and behavior for both a functional higher level representation and a lower level architectural implementation. | |
| %Secion on why AADL | |
| So why should an individual choose to use AADL rather than any of the other descriptive languages or extensions to their lexicons for defining security requirements and behavior of embedded systems? AADL is the one tool that is not only as capable and flexible as the other languages (e.g. UML), but also is easier for humans to interact with and understand from both a graphical and written standpoint. AADL also has a large community of users that have spent the past decade developing, expanding, and improving the language to meet the needs of embedded system designers across a variety of disciplines. In the following section, the paper will examine the growth of AADL as the user community expands and develops the languages capabilities to describe the function behavior of systems, detail the security requirements of models, and extension to verification tools to validate generated designs. | |
| \section{AADL Annexes and Security Extensions} | |
| \label{AADL Annexes and Extensions} | |
| \subsection{Introduction to AADL} | |
| The Architecture Analysis \& Design Language (AADL) is traditionally design for the specification, analysis, automated integration and code generation of real-time performance-critical distributed computer systems~\cite{AADLSite}. The `performance-critical' aspects of a system include timing, safety, schedulability, fault tolerance, and security. AADL works to provide a new language vehicle for allowing analysis of system designs prior to development. This language also supports model-based, model-driven development of designs throughout the life-cycle of a system or system-of-systems. The advantage being that the language and associated tools allow for developers to model, analyze, and generate embedded real-time systems while supporting model-based engineering concepts. The AADL lexicon allows for the following aspects to be described~\cite{AADLV2Overview}: | |
| \begin{enumerate} | |
| \item Precise execution semantics for components. These components are thread, process, data, subprogram, system, processor, memory, bus, device, virtual processor, virtual bus. | |
| \item Continuous control and event response processing. These are described via data and event flow, synchronous call and return, shared access, and `end-to-end' flow specifications. | |
| \item Operational modes and fault tolerant configurations. These are achieved through the use of modes and mode transitions. | |
| \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-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. | |
| \subsection{AADL Security Annex} | |
| % December 2015 Security Work | |
| Although security was not an initial concern in the development of the AADL language, there has been work made to extend the language to include behavioral and security-centric capabilities. Recent work by Ellison et.~al.~\cite{ellison2015extending} has extended the security centric properties of AADL to include user-defined `AccessGroup' and `AccessMode' properties that are used for evaluating and validating an existing system model based on user expectations of functionality, as shown in Listing~\ref{lst:AADLaccessExtension}. The extension adds different security types (e.g. unclassified, confidential, secret, top secret). When implementing these extended security properties, one must determine the viability of a system given confidentiality requirements of data objects and security clearance by users. These security extensions allow for analysis of the modeled system to ensure processes and threads are mapped to appropriate hardware, communicate over secured channels, and store data in protected memory. It also allows one to derive minimum security requirements on hardware components given a software architecture. While these two properties are effective at validating that a system will retain some arbitrary level of security, this is still not the level of detail that effectively allows for modeling of component specifications. | |
| \begin{lstlisting}[caption={User-defined AccessMode and AccessGroup properties~\cite{ellison2015extending}},label={lst:AADLaccessExtension}] | |
| property set Security_Trust is | |
| -- properties to support documenting and analyzing security | |
| -- Added property that supports access mode of data | |
| AccessProtection: list of record ( | |
| AccessMode: enumeration (r, w, rw, x); | |
| AccessGroup: enumeration (CC, ABS); | |
| ) applies to (all); | |
| end Security_Trust; | |
| \end{lstlisting} | |
| %% Add in an image of access mode and group extensions | |
| %\begin{figure} | |
| % \includegraphics[width=\textwidth]{./images/accessModeGroupExample.png} | |
| % \caption{User-defined AccessMode and AccessGroup properties~\cite{ellison2015extending}} | |
| % \label{fig:AADLaccessExtension} | |
| %\end{figure} | |
| \begin{lstlisting}[caption={Security Level Definition for AADL Security Annex~\cite{AADLSecAnnex}},label={lst:AADLSecLevels}] | |
| security_levels : list of aadlinteger => (100) applies to (all); | |
| top_secret : constant aadlinteger => 10; | |
| secret : constant aadlinteger => 40; | |
| unclassified : constant aadlinteger => 100; | |
| \end{lstlisting} | |
| %% Add in an image of new security level extensions | |
| %\begin{figure} | |
| % \includegraphics[width=\textwidth]{./images/securityLevelsExample.png} | |
| % \caption{Security Level Definition for AADL Security Annex~\cite{AADLSecAnnex}} | |
| % \label{fig:AADLSecLevels} | |
| %\end{figure} | |
| More current work on the development of a security annex for AADL has been released~\cite{AADLSecAnnex}. The concept behind this work is to extend the AADL language with a series of security annotations that will represent the security characteristics in designed architecture models. In comparison to the earlier work by Ellison et.~al.~, there is still the existence of `Security Levels' (e.g. unclassified, secret, top secret) but there are now integer values associated with each level, as shown in Listing~\ref{lst:AADLSecLevels}. | |
| %According to the information provided during the May 2016 User Days, this allows for greater compliance with other approaches such as Bell-Lapadula~\cite{AADLSecAnnex}. | |
| Other additions to the language include the definition of domains (e.g. entertainment, command and control), a level of trust, a degree of exposure, along with enumerated definitions of encryption methods and properties as well as authentication methods and implementations. In terms of security analysis tools, there has been work towards defining the attack surface in terms of how vulnerabilities are discovered within the architecture and a measurement of how safe a system is. An example of this is shown in Figure~\ref{fig:AADLAttackAnalysis}. Along the same vein, there has also been work toward generating graphical representation of vulnerabilities and their impact upon the system; similar in nature to failure mode and effect analysis or fault tree analysis. A more interesting development has been for including code generation for secure microkernel architectures such as the seL4. Unfortunately not much has been released on implementation examples of the new security annex and analysis tools as improvement is expected to continue through June 2016 with an official publication to the SEI github in July 2016~\cite{AADLSecAnalysis}. | |
| % Add in an image of attack surface graphical representation | |
| \begin{figure} | |
| \centering\includegraphics[height=6cm]{./images/attackAnalysisZoom.png} | |
| \caption{Graphical Example of AADL Security Annex Attack Impact Analysis~\cite{AADLSecAnalysis}} | |
| \label{fig:AADLAttackAnalysis} | |
| \end{figure} | |
| \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}. 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 | |
| %\begin{figure} | |
| % \includegraphics[width=\textwidth]{./images/resoluteExample.png} | |
| % \caption{Example of Resolute as a Security Property Verification Tool~\cite{ellison2015extending}} | |
| % \label{fig:AADLResoluteExample} | |
| %\end{figure} | |
| The Requirements Definition and Analysis Language Tool Environment \linebreak(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 (EMV2) 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} | |
| % \item Error types and type sets. | |
| % \item Error type mappings. | |
| % \item Error behavior state machines. | |
| % \item Error propagations and flows. | |
| % \item Component error behavior. | |
| % \item Composite error behavior. | |
| %\end{enumerate} | |
| %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 annex is 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. 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 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 | |
| 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 | |
| component or system is) coupled with a numerical value allows for a security metric for determining the | |
| possibility of attack on a specific element within a design. Both of these additional properties open the door | |
| to formalize a verification of potential security hazards and complications that may arise further down the | |
| development cycle or even once out in the field. Other additions to the AADL lexicon, such as the encryption | |
| and authentication descriptions, require that a form of library be written to allow for proper description and | |
| definition of the security-based algorithms and methods being used by different components of a system. An example of this type of definition is given in Listing~\ref{lst:AADLSecEncryption}. From a | |
| network standpoint this is highly advantageous because this also allows for a formal set of verification tools | |
| that standards and expectations are being met by all components of the design. The disadvantage of such a | |
| library is two-fold. The first issue is that in order for a security implementation library to be generated, | |
| one must rely on the knowledge of a `security expert' or `security experts' to define all the possible | |
| combinations and implementations that are currently in use. The second problem being the need to maintain such | |
| a record in a formal and standardized method. While not an impossible task, this is an issue that has plagued | |
| this sort of work~\cite{jurjens2002umlsec,jurjens2005secure}. This reliance on the knowledge and expertise of | |
| individuals may not be avoidable, in which case the current solution may be the best at hand, but is by no means | |
| a poor answer to a long standing problem. The one addition that this paper does not agree with is the move to | |
| describe the security aspect of `trust' as a non-binary value. While the released work~\cite{AADLSecAnnex} | |
| states that this scale is representative of proof of a component's correctness, this paper believes that this | |
| merging of concepts does not accurately reflect security concerns and does not allow for accurate verification | |
| and validation of security requirements and behavior. While having the language to describe and define the | |
| correctness of a component is advantageous, this is not the same as trust but should rather be seen as a | |
| combination of trust and reliability. | |
| \begin{lstlisting}[caption={AADL Security Annex Definitions of Encryption~\cite{AADLSecAnnex}},label={lst:AADLSecEncryption}] | |
| encryption : security_properties::encryption_type applies to | |
| {port, virtual bus, bus, memory, access}; | |
| encryption_type : type record ( | |
| method : security_properties::supported_encryption_method; | |
| algorithm : security properties::supported_encryption_algorithm; | |
| public_key : aadlstring; | |
| private_key : aadlstring; | |
| key : aadlstring; | |
| operation_mode : security_properties::supported_operation_mode; | |
| }; | |
| supported_encryption_method : | |
| type enumeration (symmetric, asymmetric, clear); | |
| supported_encryption)algorithm : | |
| type enumeration (tripledes, des, rsa, blowfish, aes, clear); | |
| supported_operations_mode : | |
| type enumeration (ecb, cbc, pcbc, cfb, ofb, ctr); | |
| \end{lstlisting} | |
| %% Add in an image of attack surface graphical representation | |
| %\begin{figure} | |
| % \includegraphics[width=\textwidth]{./images/encryptionExample.png} | |
| % \caption{AADL Security Annex Definitions of Encryption~\cite{AADLSecAnnex}} | |
| % \label{fig:AADLSecEncryption} | |
| %\end{figure} | |
| A prime example is the act of deciding to use hardware-based 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 generated key 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? | |
| \end{enumerate} | |
| Nowhere in this process is trust seen as a non-binary aspect. One can not say that they trust a component 80\% of the time, but they can say that they will trust a component if it is reliable 80\% of the time. In this sense, it is the deep held belief of this paper that trust should be a binary value (trusted or not trusted) while reliability can act as a supplementary value that acts as the `error bounds' by which trust is bestowed or given. A combination or mapping of trust and reliability can be given to produce a value of `component correctness', similar to how exposure is defined. | |
| %AADL is indeed a powerful and versatile language that has the potential to also act as an effective method of secure real-time embedded system design. While there has been work towards developing and improving the lack of a formalized security annex, even this work will still require the use, frustration, and feedback of the user-community to help establish a standardized tool. | |
| The greatest inadequacy of the lexicon is that there is currently no attention being given to the description and definition of high level security requirements and lower level secure component definitions that are required in order to establish and mature a tool for secure embedded system model generation and verification. While the building blocks of an effective security framework have begun to appear, there is still the need for a standardized and formal security framework in the AADL language. | |
| \section{Proposed Extensions to AADL} | |
| \label{New Framework} | |
| % Add in an image of platform-based design to illustrate the refinement process | |
| %\begin{figure} | |
| % \includegraphics[width=\textwidth]{./images/recursivePBD.png} | |
| % \caption{Visualization of Recursive PBD Model~\cite{sangiovanni2007quo}} | |
| % \label{fig:RecursivePBD} | |
| %\end{figure} | |
| As explained above, extensions to the security-centric aspects of the AADL language have been recently released but the focus of these linguistic extensions is for system analysis and code generation while not focusing on low level element properties and how to map them to higher level system requirements. As such, this paper proposes a security framework that can be adopted as an extension to AADL for the purpose of creating security model implementations mapped from security requirements and component specifications. Having examined the previous work and development of the AADL language, one can see that there is concurrent effort being placed in tracking different areas of real-time embedded system design, such as error propagation, behavior of systems and components, as well as the definition and validation of requirements. Although these extensions and annexes are not tailored specifically for security modeling needs and purposes, AADL allows for their combined use to help fill in the gaps of security requirement definition and behavior under different scenarios and conditions. The one `disadvantage' being that users will need to learn each tool separately and will be left to discover the best method of aggregate implementation; although this is truly the advantage of AADL as its own language. Considering the declared additions of a security annex extension to the AADL lexicon, there is an expansion for being able to describe said properties and aspects, but no movement yet towards verification of requirements and needs as seen with other annexes (e.g. RDALTE). There is notable work towards graphical representations of these security aspects, but again there is still a gap for the generation of secure system implementations and models. Even more of a void can be felt for a set of automated tools for exploring the security design space. | |
| % Add in an image of the drawing from the bulletjournal on the process | |
| \begin{figure} | |
| \centering\includegraphics[height=6cm]{./images/aadl_security_framework.png} | |
| \caption{Visualization of Security Framework} | |
| \label{fig:AADLSecFrame} | |
| \end{figure} | |
| 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. | |
| \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. | |
| \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. | |
| \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}. | |
| \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. | |
| % Add in the table of elements and variations | |
| \begin{table*}[] | |
| \centering | |
| \caption{Table illustrating different component variations} | |
| \label{elementTypes} | |
| \begin{tabular}{@{}llllll@{}} | |
| \toprule | |
| \multicolumn{6}{c}{Component Types Table} \\ \midrule | |
| \multicolumn{1}{c}{\multirow{2}{*}{{\underline{\textbf{Elements}}}}} & \multicolumn{5}{c}{\textbf{Types}} \\ | |
| \multicolumn{1}{c}{} & \multicolumn{1}{c}{{\underline{\textbf{I}}}} & \multicolumn{1}{c}{{\underline{ \textbf{II}}}} & \multicolumn{1}{c}{{\underline{\textbf{III}}}} & \multicolumn{1}{c}{{\underline{\textbf{IV}}}} & \multicolumn{1}{c}{{\underline{ \textbf{V}}}} \\ | |
| Memory & Unprotected & Protected & Encrypted & Obfuscated & Combo \\ | |
| Bus & Unprotected & Encrypted & Non-sniffable & & \\ | |
| Processor & Simple & Embedded Encryption & Pure Encryption & & \\ | |
| Data & Plain-text & Encryption & Protected & & \\ | |
| Port & Normal & Encrypted & Protected & & \\ \bottomrule | |
| \end{tabular} | |
| \end{table*} | |
| As shown in Table~\ref{elementTypes}, this paper has defined potential component types that would populate the architectural space of this new security framework. To show how these component elements would define a larger design, this paper moves to define and describe a `system' in this new framework. A system is defined as a grouping of elements that serve a given purpose. This grouping is created via the combination of different circuit elements to perform a specific task or function. Furthermore, this new system can be abstracted into a `single layer' device object model. | |
| 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. | |
| \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} | |
| \subsection{Security Requirements} | |
| 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. | |
| 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 should be defined via a metric derived from costs and values that | |
| represent the core elements being protected, the inherent risk of vulnerabilities associated with these elements, and the standards that must | |
| be met by a given implementation. | |
| Listing~\ref{lst:AADLUserDefineHigh} shows an example of how AADL could be used to specify security requirements. Security requirements are specified in terms of value of a service feature and impact of the feature if it was to be compromised. | |
| 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}. The advantage of this methodology being that one can connect requirements to other system artifacts, thus enabling requirement traceability and validation throughout the development process. Unfortunately the ALISA tool is still being developed and improved through implementation in industry examples and as an extension to existing system design models to show effectiveness~\cite{ALISA2016}. | |
| \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} | |
| \subsection{Mapping Process} | |
| %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. 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 disadvantage 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 | |
| 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. | |
| % 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. | |
| \section{Conclusion} | |
| \label{Conclusion} | |
| 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. | |
| With the use of the proposed security extensions to AADL, designers and developers would have an effective and efficient manner by which security implementations and models can be verified and validated, allowing for visibility in the early phase design process and ideally saving time. Defining, formally describing, and validation of security needs and requirements is paramount to the future design and development of real-time embedded systems, especially with the growth of the Internet-of-Things (IoT) devices. There is a need for methods and tools that will allow for exploration of the entire design space. Further automation of such tools is the most efficient manner for generating secure model implementations based on requirements and specifications. Future work includes: formulation of a mapping process to take security requirements and component specifications as input and output model implementations that can be verified and validated. Verification tools for validating generated model implementations need to be developed. Lastly, augmenting this paper's efforts towards creating a better security framework by coupling the use of existing AADL annexes and tools (e.g. BLESS and EMV2) to allow for modeling of security behavior. Ultimately, this paper believes that AADL, its extensive user-community, and inherent extensibility make it the best linguistic tool to achieve the goal of a formalized, effective, security framework for design model generation and verification. | |
| % | |
| % ---- Bibliography ---- | |
| % | |
| \begin{thebibliography}{5} | |
| \bibitem {SysML-Sec} | |
| SysML-Sec, | |
| \url{http://sysml-sec.telecom-paristech.fr/} | |
| \bibitem {jurjens2005secure} | |
| J{\"u}rjens, J.: | |
| Secure systems development with UML, | |
| Springer Science \& Business Media (2005) | |
| \bibitem {jurjens2002umlsec} | |
| J{\"u}rjens, J.: | |
| UMLsec: Extending UML for secure systems development, | |
| UML 2002—The Unified Modeling Language, Springer Publishing, pages 412--425 (2002) | |
| \bibitem {SysML} | |
| SysML, | |
| \url{http://sysml.org/} | |
| \bibitem {AADLSite} | |
| AADL, | |
| \url{http://www.aadl.info/aadl/currentsite/} | |
| \bibitem {AADLV2Overview} | |
| Feiler, P.: | |
| SAE AADL V2: An Overview. | |
| Carnegie Mellon University (2010) | |
| \bibitem {AADLTools} | |
| AADL Tools, | |
| \url{https://wiki.sei.cmu.edu/aadl/index.php/AADL\_tools} | |
| \bibitem {Osate2} | |
| Osate 2, | |
| \url{https://wiki.sei.cmu.edu/aadl/index.php/Osate\_2} | |
| \bibitem {Osate2Examples} | |
| Osate 2 Example Repository, | |
| \url{https://github.com/osate/examples} | |
| \bibitem {UserDaysMay2016} | |
| User Days - May 2016, | |
| \url{https://github.com/saeaadl/userdays/tree/master/UserDays/May2016} | |
| \bibitem {AADLResolute} | |
| Resolute Website, | |
| \url{http://loonwerks.com/tools/resolute.html} | |
| \bibitem {RDALOverview} | |
| Blouin, D.: | |
| AADL Requirements Annex Review, | |
| \url{http://www.aadl.info/aadl/downloads/committee/feb2013/presentations/aadl\_standards\_requirements\_annex\_review\_06022013.pdf} | |
| \bibitem {gacek2014resolute} | |
| Gacek, A., Backes, J., Cofer, D., Slind, K., Whalen, M.: | |
| Resolute: An assurance case language for architecture models, | |
| ACM SIGAda Ada Letters, Volume 34 Number 3, pages 19--28 (2014) | |
| \bibitem {EMV1} | |
| Feiler, P.: | |
| SAE AADL Error Model Annex: An Overview, | |
| \url{https://wiki.sei.cmu.edu/aadl/images/1/13/ErrorModelOverview-Sept222011-phf.pdf} | |
| \bibitem {EMV2} | |
| Feiler, P.: | |
| SAE AADL Error Model Annex: Discussion Items, | |
| \url{https://wiki.sei.cmu.edu/aadl/images/1/13/ErrorModelOverview-Sept222011-phf.pdf} | |
| \bibitem {BLESS2013} | |
| Larson, B.R., Chalin, P., Hatcliff, J.: | |
| BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software, | |
| \url{https://ti.arc.nasa.gov/m/events/nfm2013/pubs/BLESS.pdf} | |
| \bibitem {AADLSecAnnex} | |
| Delange, J., Feiler, P., Klieber, W., Nam, M., Seibel, J.: | |
| AADL Security Annex, | |
| \url{https://github.com/saeaadl/userdays/blob/master/UserDays/May2016/security-annex-May2016.pdf} | |
| \bibitem {AADLSecAnalysis} | |
| Delange, J., Nam, M., Seibel, J.: | |
| AADL Security Analysis Tools, | |
| \url{https://github.com/saeaadl/userdays/blob/master/UserDays/May2016/security-analysis-May2016.pdf} | |
| \bibitem {ellison2015extending} | |
| Ellison, R., Householder, A., Hudak, J., Kazman, R., Woody, C.: | |
| Extending AADL for Security Design Assurance of Cyber-Physical Systems, | |
| Software Engineering Institute, CMU/SEI-2015-TR-014 (2015) | |
| \bibitem {jeepHack} | |
| Drozhzhin, A.: | |
| Black Hat USA 2015: The full story of how that Jeep was hacked, | |
| \url{https://blog.kaspersky.com/blackhat-jeep -cherokee-hack-explained/9493/} | |
| \bibitem {planeHack} | |
| Zetter, K.: | |
| Feds say that banned researcher commandeered a plane, | |
| \url{http://www.wired.com/2015/05/feds-say-banned-researcher-commandeered-plane/} | |
| \bibitem {superFish} | |
| Hope, P.: | |
| Superfish adware weakens security and injects ads on some Lenovo laptops, | |
| \url{http://www.techrepublic.com/article/superfish-adware-weakens-security-and-injects-ads-on-some-lenovo-laptops/} | |
| \bibitem {lenovoWPBT} | |
| Sanders, J.: | |
| Windows and UEFI anti-theft mechanism makes systems less secure, | |
| \url{http://www.techrepublic.com/article/windows-and -uefi-anti-theft-mechanism-makes-systems-less-secure/} | |
| \bibitem {govHack} | |
| Olorunnipa, T.: | |
| Breach of Employee Data Wider Than Initial Report, U.S. Says, | |
| \url{http://www.bloomberg.com/politics/articles/2015-06-12/white-house-says-personnel-records-possibly-breached-twice} | |
| \bibitem {stageFright} | |
| Vaughan-Nicholas, S.J.: | |
| Stagefright: Just how scary is it for Android users?, | |
| \url{http://www.zdnet.com/article/stagefright-just-how-scary-is-it-for-android-users/} | |
| \bibitem {stageFright2} | |
| Whittaker, Z.: | |
| Stagefright is back, and affecting millions of Android devices, | |
| \url{http://www.zdnet.com/article/new-stagefright-2-0-flaws-affect-millions-of-android-devices/} | |
| \bibitem {androidUpdates} | |
| Tofel, K.: | |
| HTC says monthly Android security updates are ``unrealistic'', | |
| \url{http://www.zdnet.com/article/htc-says-monthly-stagefright-android-security-updates-are-unrealistic/} | |
| \bibitem {androidMarshmallow} | |
| Jack Wallen, J.: | |
| The woes of Android updates, and how to fix the process, | |
| \url{http://www.techrepublic.com/article/the-woes-of-android-updates-and-how-to-fix-the-process/} | |
| \bibitem {googleAndroid} | |
| Sanders, J.: | |
| Google finally doubles down on security with monthly Android updates, | |
| \url{http://www.techrepublic.com/article/google-and-some -android-phone-vendors-introduce-welcome-changes-to-security-update-process/} | |
| \bibitem {aaraj2008analysis} | |
| Aaraj, N., Raghunathan, A., Jha, N.K.: | |
| Analysis and design of a hardware/software trusted platform module for embedded systems, | |
| ACM Transactions on Embedded Computing Systems (TECS), Volume 8 Number 1, page 8 (2008) | |
| \bibitem {denning1996location} | |
| Denning, D.E., MacDoran, P.F.: | |
| Location-based authentication: Grounding cyberspace for better security, | |
| Computer Fraud \& Security, Volume 1996 Number 2, pages 12--16 (1996) | |
| \bibitem {saito2015case} | |
| Saito, M., Hazeyama, A., Yoshioka, N., Kobashi, T., Washizaki, H., Kaiya, H., Ohkubo, T.: | |
| A case-based management system for secure software development using software security knowledge, | |
| Procedia Computer Science, Volume 60, pages 1092--1100 (2015) | |
| \bibitem {denning2015toward} | |
| Denning, D.E.: | |
| Toward more secure software, | |
| Communications of the ACM, Volume 8 Number 4, pages 24--26 (2015) | |
| \bibitem {nguyen2015model} | |
| Nguyen, P.: | |
| Model-Driven Security With Modularity and Reusability For Engineering Secure Software Systems, | |
| University of Luxembourg (2015) | |
| \bibitem {ravi2004security} | |
| Ravi, S., Raghunathan, A., Kocher, P., Hattangady, S.: | |
| Security in embedded systems: Design challenges, | |
| ACM Transactions on Embedded Computing Systems (TECS), Volume 3 Number 3, pages 461--491 (2004) | |
| \bibitem {gokhale2008model} | |
| Gokhale, A., Balasubramanian, K., Krishna, A.S., Balasubramanian, J., Edwards, G., Deng, G., Turkay, E., Parsons, J., Schmidt, D.C.: | |
| Model driven middleware: A new paradigm for developing distributed real-time and embedded systems, | |
| Science of Computer programming, Volume 73 Number 1, pages 39--58 (2008) | |
| \bibitem {perez2006vtpm} | |
| Perez, R., Sailer, R., van Doorn, L., and others: | |
| vTPM: virtualizing the trusted platform module, | |
| Proc. 15th Conf. on USENIX Security Symposium, pages 305--320 | |
| \bibitem {yan2015novel} | |
| Yan, W., Tehranipoor, F., Chandy, J.A.: | |
| A Novel Way to Authenticate Untrusted Integrated Circuits, | |
| Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, pages 132--138 (2015) | |
| \bibitem {tehranipoor2015dram} | |
| Tehranipoor, F., Karimina, N., Xiao, K., Chandy, J.: | |
| DRAM based intrinsic physical unclonable functions for system level security, | |
| Proceedings of the 25th edition on Great Lakes Symposium on VLSI, pages 15--20 (2015) | |
| \bibitem {CommonCriteria} | |
| Common Criteria for Information Technology Security Evaluation, | |
| ISO/IEC, Number ISO/IEC 15408, July 2015 | |
| \bibitem {benzel2005design} | |
| Benzel, T.V., Irvine, C.E., Levin, T.E., Bhaskara, G., Nguyen, T.D., Clark, P.C.: | |
| Design principles for security (2005) | |
| \bibitem {lin2013security} | |
| Lin, C., Zhu, Q., Phung, C., Sangiovanni-Vincentelli, A.: | |
| Security-aware mapping for CAN-based real-time distributed automotive systems, | |
| Computer-Aided Design (ICCAD), 2013 IEEE/ACM International Conference on, pages 115--121 (2013) | |
| \bibitem {markose2008systematic} | |
| Markose, S., Liu, X., McMillin, B.: | |
| A systematic framework for structured object-oriented security requirements analysis in embedded systems, | |
| IEEE/IFIP International Conference on Embedded and Ubiquitous Computing, 2008. EUC'08, Volume 1, pages 75--81 (2008) | |
| \bibitem {yu1997towards} | |
| Yu, E.S.: | |
| Towards modelling and reasoning support for early-phase requirements engineering, | |
| Proceedings of the Third IEEE International Symposium on Requirements Engineering, pages 226--235 (1997) | |
| \bibitem {massacci2010security} | |
| Massacci, F., Mylopoulos, J., Zannone, N.: | |
| Security requirements engineering: the SI* modeling language and the secure tropos methodology, | |
| Advances in Intelligent Information Systems, pages 147--174 (2010) | |
| \bibitem {sangiovanni2007quo} | |
| 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} |