Abstract
Cyber-physical systems are generally composed of several software components executing on different processors that are interconnected through entities that can be represented as buses. These complex systems collocate functions operating at different security levels, which can introduce unexpected interactions that affect system security. The security policy for these systems is realized through various complex physical or logical mechanisms. The security policy, as a stakeholder goal, is then refined into system requirements and implementation constraints that are used to guarantee security objectives. Unfortunately, verifying the correct decomposition and its enforcement in the system architecture is an overwhelming task. To overcome these issues, requirements must be clearly specified and traced through the system architecture, and automatically verified throughout the development process.
In this report, we introduce a modeling framework for the design and validation of requirements from a security perspective. It is composed of a new language for requirements specification, an extension of the Architecture Analysis & Design Language, for specifying security and a set of theorems to check the requirements against the architecture. The framework provides the capability to validate the requirements of several candidate architectures and reiterate models to cope with the impact of changes to requirements and architecture during development. This model-based approach helps software architects and developers detect requirements and architecture issues early in the development life cycle and avoid the propagation of their effects during integration.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Dvorak, D.L.: NASA Study on Flight Software Complexity (2009)
National Institute of Standards and Technology: The Economic Impacts of Inadequate Infrastructure for Software Testing. Technical report, NIST (2002)
SAE International: AS5506 - Architecture Analysis and Design Language (AADL) (2012)
Redman, D., Ward, D., Chilenski, J., Pollari, G.: Virtual Integration for Improved System Design: The AVSI System Architecture Virtual Integration (SAVI) Program. Analytic Virtual Integration of Cyber-Physical Systems Workshopp, 31st IEEE Real-Time Systems Symposium (RTSS 2010) (2010)
Backes, J., Cofer, D., Miller, S., Whalen, M.W.: Requirements analysis of a quad-redundant flight control system. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 82–96. Springer, Heidelberg (2015)
Kelly, T.: A systematic approach to safety case management. In: Proceedings of SAE 2004 World Congress, Detroit, MI (2004)
Kobayashi, N., Yamamoto, S.: The effectiveness of D-case application knowledge on a safety process. Procedia Comput. Sci. 60, 908–917 (2015). 19th Annual Conference on Knowledge-Based and Intelligent Information and Engineering Systems, KES-2015, Singapore, Proceedings, September 2015
Hawkins, R., Kelly, T., Habli, I.: Developing assurance cases for D-MILS systems. In: International Workshop on MILS: Architecture and Assurance for Secure Systems, Amsterdam, The Netherlands, January 2015
Gacek, A., Backes, J., Cofer, D., Slind, K., Whalen, M.: Resolute: an assurance case language for architecture models. In: Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology. HILT 2014. ACM, New York (2014)
Blouin, D., Senn, E., Turki, S.: Defining an annex language to the architecture analysis and design language for requirements engineering activities support. In: Model-Driven Requirements Engineering Workshop (MoDRE), 2011, pp. 11–20, August 2011
Delange, J., Feiler, P., Ernst, N.: Incremental life cycle assurance of safety-critical systems. In: 8th European Congress ERTS, Toulouse (2016)
Van der Pol, K., Noll, T.: Security type checking for MILS-AADL specifications. In: International Workshop on MILS: Architecture and Assurance for Secure Systems, Amsterdam, The Netherlands, January 2015
Alsaleh, M.N., Al-Shaer, E., El-Atawy, A.: Towards a unified modeling and verification of network and system security configurations. In: Al-Shaer, E., Ou, X., Xie, G. (eds.) Automated Security Management, pp. 3–19. Springer, Cham (2013)
Bell, D.E., LaPadula, L.J.: Secure computer system: unified exposition and MULTICS interpretation. Technical report, The MITRE Corporation, Bedford, MA (1976)
Biba, K.J.: Integrity considerations for secure computer systems. Technical report, The MITRE Corporation, Bedford, MA (1977)
Lipner, S.B.: The birth and death of the orange book. IEEE Ann. Hist. Comput. 37(2), 19–31 (2015)
Alves-Foss, J., Harrison, W.S., Oman, P., Taylor, C.: The MILS architecture for high-assurance embedded systems. Intl. J. Embed. Syst. 2(3/4), 239–247 (2005)
IEEE Center of Secure Design: Avoiding the TOP 10 Software Security Design Flaws. Technical report, IEEE (2014)
Zalila, B., Hamid, I., Hugues, J., Pautet, L.: Generating distributed high integrity applications from their architectural description. In: Abdennadher, N., Kordon, F. (eds.) Ada-Europe 2007. LNCS, vol. 4498, pp. 155–167. Springer, Heidelberg (2007)
Larson, B., Hatcliff, J., Fowler, K., Delange, J.: Illustrating the AADL error modeling annex (V.2) using a simple safety-critical medical device. In: Proceedings of the 2013 ACM SIGAda Annual Conference on High Integrity Language Technology, HILT 2013, pp. 65–84. ACM, New York (2013)
Shiraishi, S.: An AADL-based approach to variability modeling of automotive control systems. In: Petriu, D.C., Rouquette, N., Haugen, Ø. (eds.) MODELS 2010, Part I. LNCS, vol. 6394, pp. 346–360. Springer, Heidelberg (2010)
Aldrich, B., Fehnker, A., Feiler, P.H., Han, Z., Krogh, B.H., Lim, E., Sivashankar, S.: Managing verification activities using SVM. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 61–75. Springer, Heidelberg (2004)
Massol, V., Husted, T.: JUnit in Action. Manning, Stamford (2003)
Warmer, J.B., Kleppe, A.G.: The Object Constraint Language: Getting Your Models Ready for MDA. Addison-Wesley Professional, Boston (2003)
Matsuno, Y., Takamura, H., Ishikawa, Y.: A dependability case editor with pattern library. In: 2010 IEEE 12th International Symposium on High-Assurance Systems Engineering (HASE), pp. 170–171, November 2010
Miller, C., Valasek, C.: Remote Exploitation of an Unaltered Passenger Vehicle. Black Hat USA (2015)
Acknowledgments
This material is based upon work funded and supported by the Department of Defense under Contract No. FA8721-05-C-0003 with Carnegie Mellon University for the operation of the Software Engineering Institute, a federally funded research and development center.
[Distribution Statement A] This material has been approved for public release and unlimited distribution. Please see Copyright notice for non-US Government use and distribution.
DM-0003481.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Nam, MY., Delange, J., Feiler, P. (2016). Integrated Modeling Workflow for Security Assurance. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_64
Download citation
DOI: https://doi.org/10.1007/978-3-319-47166-2_64
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47165-5
Online ISBN: 978-3-319-47166-2
eBook Packages: Computer ScienceComputer Science (R0)