Yongwang Zhao
Skip Abstract Section
Abstract
Assurance of information-flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for improving safety, ARINC 653 has been complied with by mainstream separation kernels. Due to the new trend of integrating safe and secure functionalities into one separation kernel, security analysis of ARINC 653 as well as a formal specification with security proofs are thus significant for the development and certification of
- G. Parr and R. Edwards, “ Integrated modular avionics,” Air Space Europe, vol. Volume 1, no. Issue 2, pp. 72–75, 1999.Google Scholar
Cross Ref
- AUTOSAR Specifications (Release 4.2), AUTOSAR GbR, Munchen, Germany, 2015.Google Scholar
- J. Rushby, “ Design and verification of secure systems,” ACM SIGOPS Operating Syst. Rev., vol. Volume 15, no. Issue 5, pp. 12–21, 1981. Google ScholarDigital Library
- J. Rushby, “ Partitioning in avionics architectures: Requirements, mechanisms, and assurance,” <institution>U.S. Dept. Transp., Federal Aviation Administration</institution>, Washington, D.C., USA, Tech. Rep. DOT/FAA/AR-99/58, 2000.Google Scholar
- ARINC Specification 653: Avionics Application Software Standard Interface, Part 1-Required Services, Aeronautical Radio, Inc., Annapolis, MD, USA, 2010.Google Scholar
- Common Criteria for Information Technology Security Evaluation, 3rd ed. Fort Meade, MD, USA: Nat. Secur. Agency, 2012.Google Scholar
- U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, Fort Meade, MD, USA: Nat. Secur. Agency, 2007.Google Scholar
- I. Craig, Formal Refinement for Operating System Kernels . New York, NY, USA: Springer, 2007. Google ScholarDigital Library
- A. Velykis and L. Freitas, “ Formal modelling of separation kernel components,” in Theoretical Aspects of Computing, Berlin, Germany: Springer, 2010, pp. 230–244. Google ScholarDigital Library
- F. Verbeek, et al., “ Formal specification of a generic separation kernel,” Archive Formal Proofs, 2014, http://www.isa-afp.org/entries/CISC-Kernel.shtmlGoogle Scholar
- F. Verbeek, et al., “ Formal API specification of the PikeOS separation kernel,” in NASA Formal Methods, Berlin, Germany: Springer, 2015, pp. 375–389.Google Scholar
- C. Heitmeyer, M. Archer, E. Leonard, and J. McLean, “ Applying formal methods to a certifiably secure software system,” IEEE Trans. Software Eng., vol. Volume 34, no. Issue 1, pp. 82–98, 2008. Google ScholarDigital Library
- R. Richards, “ Modeling and security analysis of a commercial real-time operating system kernel,” in Design and Verification of Microprocessor Systems for High-Assurance Applications . Berlin, Germany: Springer, 2010, pp. 301–322.Google Scholar
- M. Wilding, D. Greve, R. Richards, and D. Hardin, “ Formal verification of partition management for the AAMP7G microprocessor,” in Design and Verification of Microprocessor Systems for High-Assurance Applications . Berlin, Germany: Springer, 2010, pp. 175–191.Google Scholar
- L. Freitas and J. McDermott, “ Formal methods for security in the Xenon hypervisor,” Int. J. Softw. Tools Technol. Transfer, vol. Volume 13, no. Issue 5, pp. 463–489, 2011.Google ScholarCross Ref
- T. Murray, et al., “ seL4: From general purpose to a proof of information flow enforcement,” in Proc. IEEE Symp. Secur. Privacy, May 2013, pp. 415–429. Google ScholarDigital Library
- M. Dam, R. Guanciale, N. Khakpour, H. Nemati, and O. Schwarz, “ Formal verification of information flow security for a simple arm-based separation kernel,” in Proc. ACM SIGSAC Conf. Comput. Commun. Secur., Nov. 2013, pp. 223–234. Google ScholarDigital Library
- D. Sanán, A. Butterfield, and M. Hinchey, “ Separation kernel verification: The Xtratum case study,” in Verified Software: Theories, Tools and Experiments . Berlin, Germany: Springer, 2014, pp. 133–149.Google Scholar
- M. Clarkson and F. Schneider, “ Hyperproperties,” J. Comput. Secur., vol. Volume 18, no. Issue 6, pp. 1157–1210, 2010. Google ScholarDigital Library
- J. Rushby, “ Noninterference, transitivity, and channel-control security policies,” <institution>SRI Int., Comput. Sc. Laboratory</institution>, Menlo Park, CA, USA, Tech. Rep. CSL-92–02, 1992.Google Scholar
- A. Sabelfeld and A. Myers, “ Language-based information-flow security,” IEEE J. Sel. Areas Commun., vol. Volume 21, no. Issue 1, pp. 5–19, 2003. Google ScholarDigital Library
- D. Oheimb, “ Information flow control revisited: Noninfluence = Noninterference+ Nonleakage,” in Computer Security, Berlin, Germany: Springer, 2004, pp. 225–243.Google Scholar
- T. Murray, D. Matichuk, M. Brassil, P. Gammie, and G. Klein, “ Noninterference for operating system kernels,” in Certified Programs and Proofs, Berlin, Germany: Springer, 2012, pp. 126–142. Google ScholarDigital Library
- R. Back and K. Sere, “ Stepwise refinement of action systems,” in Mathematics of Program Construction . Berlin, Germany: Springer, 1989, pp. 115–138. Google ScholarDigital Library
- N. Wirth, “ Program development by stepwise refinement,” Commun. ACM, vol. Volume 14, no. Issue 4, pp. 221–227, 1971. Google ScholarDigital Library
- R. Back and K. Sere, “ Superposition refinement of reactive systems,” Formal Aspects Comput., vol. Volume 8, no. Issue 3, pp. 324–346, 1996. Google ScholarCross Ref
- J. Abrial and S. Hallerstede, “ Refinement, decomposition, and instantiation of discrete models: Application to event-B,” Fundamenta Informaticae, vol. Volume 77, no. Issue 1/2, pp. 1–28, 2007. Google ScholarDigital Library
- G. Klein, et al., “ Comprehensive formal verification of an OS microkernel,” ACM Trans. Comput. Syst., vol. Volume 32, no. Issue 1, pp. 2:1–2:70, 2014. Google ScholarDigital Library
- Y. Zhao, Z. Yang, D. Sanan, and Y. Liu, “ Event-based formalization of safety-critical operating system standards: An experience report on ARINC 653 using event-B,” in Proc. IEEE 26th Int. Symp. Software Rel. Eng., Nov. 2015, pp. 281–292. Google ScholarDigital Library
- A. Gomes, “ Formal specification of the ARINC 653 architecture using circus,” <named-content content-type=ref-degree>Master's thesis</named-content>, <institution>Dept. Comput. Sci., Univ.</institution>York, York, U.K., 2012.Google Scholar
- J. Delange, L. Pautet, and F. Kordon, “ Modeling and validation of ARINC653 architectures,” in Proc. Embedded Real Time Software Syst., May 2010, pp. 1–8.Google Scholar
- P. Cámara, J. Castro, M. Gallardo, and P. Merino, “ Verification support for ARINC-653-based avionics software,” Softw. Testing Verification Rel., vol. Volume 21, no. Issue 4, pp. 267–298, 2011.Google Scholar
- T. Nipkow, M. Wenzel, and L. Paulson, Isabelle/HOL: A Proof Assistant for Higher-Order Logic . Berlin, Germany: Springer, 2002. Google ScholarDigital Library
- A. Crespo, I. Ripoll, and M. Masmano, “ Partitioned embedded architecture based on hypervisor: The XtratuM approach,” in Proc. Eur. Dependable Comput. Conf., Apr. 2010, pp. 67–72. Google ScholarDigital Library
- J. Delange, and L. Lec, “ POK, an ARINC 653-compliant operating system released under the BSD license,” in Proc. 13th Real-Time Linux Workshop, Oct. 2011, pp. 1–13.Google Scholar
- J. Millen, “ 20 years of covert channel modeling and analysis,” in Proc. IEEE Symp. Secur. Privacy, May 1999, pp. 113–114.Google ScholarCross Ref
- Y. Zhao, D. Sanan, F. Zhang, and Y. Liu, “ Reasoning about information flow security of separation kernels with channel-based communication,” in Proc. 22nd Int. Conf. Tools Algorithms Construction Anal. Syst., Apr. 2016, pp. 791–810. Google ScholarDigital Library
- J. Goguen and J. Meseguer, “ Security policies and security models,” in Proc. IEEE Symp. Secur. Privacy, Apr. 1982, pp. 11–20.Google ScholarCross Ref
- H. Mantel and D. Sands, “ Controlled declassification based on intransitive noninterference,” in Proc. 2nd Asian Symp. Program. Languages Syst., Nov. 2004, pp. 129–145.Google ScholarCross Ref
- M. Krohn and E. Tromer, “ Noninterference for a practical DIFC-based operating system,” in Proc. 30th IEEE Symp. Secur. Privacy, May 2009, pp. 61–76. Google ScholarDigital Library
- A. G. Ramirez, J. Schmaltz, F. Verbeek, B. Langenstein, and H. Blasum, “ On two models of noninterference: Rushby and greve, wilding, and vanfleet,” in Proc. 33rd Int. Conf. Comput. Safety Rel. Secur., Sep. 2014, pp. 246–261. Google ScholarDigital Library
- T. Levin, C. Irvine, C. Weissman, and T. Nguyen, “ Analysis of three multilevel security architectures,” in Proc. ACM Workshop Comput. Secur. Archit., Oct. 2007, pp. 37–46. Google ScholarDigital Library
- M. Clarkson, B. Finkbeiner, M. Koleini, K. Micinski, M. Rabe, and C. Sánchez, “ Temporal logics for hyperproperties,” in Principles of Security and Trust, Berlin, Germany: Springer, 2014, pp. 265–284.Google Scholar
- S. Eggert, R. Van der Meyden, H. Schnoor, and T. Wilke, “ The complexity of intransitive noninterference,” in Proc. Symp. Secur. Privacy, May 2011, pp. 196–211. Google ScholarDigital Library
- V. Ha, M. Rangarajan, D. Cofer, H. Rues, and B. Dutertre, “ Feature-based decomposition of inductive proofs applied to real-time avionics software: An experience report,” in Proc. 26th Int. Conf. Software Eng., May 2004, pp. 304–313. Google ScholarDigital Library
- G. Klein, “ Operating system verification-an overview,” Sadhana, vol. Volume 34, no. Issue 1, pp. 27–69, 2009.Google ScholarCross Ref
- J. Andronick, et al., “ Large-scale formal verification in practice: A process perspective,” in Proc. 34th Int. Conf. Softw. Eng., Jun. 2012, pp. 1002–1011. Google ScholarDigital Library
- H. Blasum, et al., “ Used formal methods,” White Paper, EURO-MILS, 2015.Google Scholar
- T. S. Hoang, “ Security invariants in discrete transition systems,” Formal Aspects Comput., vol. Volume 25, no. Issue 1, pp. 59–87, 2013. Google ScholarCross Ref
- D. McCullough, “ Noninterference and the composability of security properties,” in Proc. IEEE Conf. Secur. Privacy, Apr. 1988, pp. 177–186. Google ScholarDigital Library
- R. Richards, D. Greve, and M. Wilding, “ The common criteria, formal methods and ACL2,” presented at the ACL2 Workshop, Austin, TX, USA, 2004.Google Scholar
- D. Sanan, Y. Zhao, and H. Zhe, et al., “ CSimpl: A rely-guarantee-based framework for verifying concurrent programs,” in Proc. 23rd Int. Conf. Tools Algorithms for Construction Anal. Syst., 2017, to appear. Google ScholarDigital Library
Recommendations
Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication
Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636Assurance of information flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for separation kernels, ARINC 653 has been complied with by mainstream separation kernels. Security of ...
Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-B
ARINC 653 as the de facto standard of partitioning operating systems has been applied in many safety-critical domains. The multi-core version of ARINC 653, ARINC 653 Part 1-4 (Version 4), provides support for services to be utilized with a module that ...
Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP
This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
Comments