Multi-timed Noninterference Verification
Author:
Affiliation:

Clc Number:

TP311

  • Article
  • | |
  • Metrics
  • |
  • Reference [41]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    Safety-critical embedded software usually has rigorous time constraints over the runtime behaviors, raising additional requirements for enforcing security properties. To protect the information flow security of embedded software and mitigate the limitations of the existing simplex verification approaches and their potential false positives, this study first proposes a new timed noninterference property, i.e., timed SIR-NNI, based on the security requirement of a realistic scenario. Then the study presents an information flow security verification approach that unifies the verification of multiple timed noninterference properties, i.e., timed BNNI, timed BSNNI, and timed SIR-NNI. Based on the different timed noninterference requirements, the approach constructs the refined automata and test automata from the timed automata under verification. The study uses UPPAAL’s reachability analysis to implement the refinement relation check and the security verification. The verification tool, i.e., TINIVER, extracts timed automata from SysML’s sequential diagrams or C++ source code to conduct the verification procedure. The verification results of TINIVER on existing timed automata models and security properties justify the usability of the proposed approach. The security verifications on the typical flight-mode switch models of the UAV flight control systems ArduPilot and PX4 demonstrate the practicability and scalability of the proposed approach. Besides, the approach is effective in mitigating the false positives of a state-of-the-art verification approach.

    Reference
    [1] Goguen JA, Meseguer J. Security policies and security models. In: Proc. of the 1982 IEEE Symp. on Security and Privacy. Oakland: IEEE, 1982. 11–20.
    [2] Focardi R, Gorrieri R. The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering, 1997, 23(9): 550–571. [doi: 10.1109/32.629493]
    [3] Van Der Meyden R, Zhang CY. Algorithmic verification of noninterference properties. Electronic Notes in Theoretical Computer Science, 2007, 168: 61–75. [doi: 10.1016/j.entcs.2006.11.002]
    [4] Sabelfeld A, Myers AC. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 2003, 21(1): 5–19. [doi: 10.1109/JSAC.2002.806121]
    [5] Cassez F, van der Meyden R, Zhang CY. The complexity of synchronous notions of information flow security. In: Proc. of the 13th Int’l Conf. on Foundations of Software Science and Computational Structures. Paphos: Springer, 2010. 282–296.
    [6] 张帆, 徐明迪, 赵涵捷, 张聪, 刘小丽, 胡方宁. 软件实时可信度量: 一种无干扰行为可信性分析方法. 软件学报, 2019, 30(8): 2268-2286. http://www.jos.org.cn/1000-9825/5768.htm
    Zhang F, Xu MD, Zhao HC, Zhang C, Liu XL, Hu FN. Real-time trust measurement of software: Behavior trust analysis approach based on noninterference. Ruan Jian Xue Bao/Journal of Software, 2019, 30(8): 2268-2286 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5768.htm
    [7] Clarkson MR, Finkbeiner B, Koleini M, Micinski KK, Rabe MN, Sánchez C. Temporal logics for hyperproperties. In: Proc. of the 3rd Int’l Conf. on Principles of Security and Trust. Grenoble: Springer, 2014. 265–284.
    [8] Bonakdarpour B, Prabhakar P, Sánchez C. Model checking timed hyperproperties in discrete-time systems. In: Proc. of the 12th NASA Formal Methods Symp. Moffett Field: Springer, 2020. 311–328.
    [9] Ho HM, Zhou RY, Jones TM. Timed hyperproperties. Information and Computation, 2021, 280: 104639. [doi: 10.1016/j.ic.2020.104639]
    [10] Focardi R, Gorrieri R. Classification of security properties (Part I: Information flow). In: Proc. of the 2000 Int’l School on Foundations of Security Analysis and Design. Berlin: Springer, 2000. 331–396.
    [11] Lee M, D’Argenio PR. A refinement based notion of non-interference for interface automata: Compositionality, decidability and synthesis. In: Proc. of the 2010 XXIX Int’l Conf. of the Chilean Computer Science Society. Antofagasta: IEEE, 2010. 280–289.
    [12] 李沁, 曾庆凯, 袁志祥. 一种面向非干扰的线程程序逻辑. 软件学报, 2014, 25(6): 1143-1153. http://www.jos.org.cn/1000-9825/4429.htm
    Li Q, Zeng QK, Yuan ZX. Logic of multi-threaded programs for non-interference. Ruan Jian Xue Bao/Journal of Software, 2014, 25(6): 1143-1153 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4429.htm
    [13] Sun C, Xi N, Li JK, Yao QS, Ma JF. Verifying secure interface composition for component-based system designs. In: Proc. of the 21st Asia-Pacific Software Engineering Conf. Jeju: IEEE, 2014. 359–366.
    [14] Sun C. SysML2ia. 2020. https://bitbucket.org/suncong_xdu/sysml2ia/src/master/
    [15] Sun C, Xi N, Ma JF. Enforcing generalized refinement-based noninterference for secure interface Composition. In: Proc. of the 41st IEEE Annual Computer Software and Applications Conf. Turin: IEEE, 2017. 586–595.
    [16] Sun C. CertIA: A coq library for certifying interface automata. 2020. https://github.com/suncongxd/certia
    [17] 谢钧, 黄皓. 一个非确定系统的不干扰模型. 软件学报, 2006, 17(7): 1601-1608. http://www.jos.org.cn/jos/article/abstract/20060714?st=search
    Xie J, Huang H. A noninterference model for nondeterministic systems. Ruan Jian Xue Bao/Journal of Software, 2006, 17(7): 1601-1608 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/17/1601.htm
    [18] Jiang K, Zhang TW, Sanán D, Zhao YW, Liu Y. A formal methodology for verifying side-channel vulnerabilities in cache architectures. In: Proc. of the 23rd Int’l Conf. on Formal Engineering Methods, Formal Methods and Software Engineering (ICFEM 2022). Madrid: Springer, 2022. 190–208.
    [19] Gray III JW. Toward a mathematical foundation for information flow security. Journal of Computer Security, 1992, 1(3–4): 255–294. [doi: 10.3233/JCS-1992-13-405]
    [20] Gerking C, Schubert D. Component-based refinement and verification of information-flow security policies for cyber-physical microservice architectures. In: Proc. of the 2019 IEEE Int’l Conf. on Software Architecture. Hamburg: IEEE, 2019. 61–70.
    [21] Focardi R, Gorrieri R, Martinelli F. Real-time information flow analysis. IEEE Journal on Selected Areas in Communications, 2003, 21(1): 20–35. [doi: 10.1109/JSAC.2002.806122]
    [22] Gardey G, Mullins J, Roux OH. Non-interference control synthesis for security timed automata. Electronic Notes in Theoretical Computer Science, 2007, 180(1): 35–53. [doi: 10.1016/j.entcs.2005.05.046]
    [23] Benattar G, Cassez F, Lime D, Roux OH. Control and synthesis of non-interferent timed systems. International Journal of Control, 2015, 88(2): 217–236. [doi: 10.1080/00207179.2014.944356]
    [24] Gorrieri R, Locatelli E, Martinelli F. A simple language for real-time cryptographic protocol analysis. In: Proc. of the 12th European Symp. on Programming. Warsaw: Springer, 2003. 114–128.
    [25] Vasilikos P, Nielson F, Nielson HR. Secure information release in timed automata. In: Proc. of the 7th Int’l Conf. on Principles of Security and Trust. Thessaloniki: Springer, 2018. 28–52.
    [26] Gerking??????桨瑵浢?扲牴?D, Bodden E. Model checking the information flow security of real-time systems. In: Proc. of the 10th Int’l Symp. on Engineering Secure Software and Systems. Paris: Springer, 2018. 27–43.
    [27] Heinzemann C, Brenner C, Dziwok S, Schäfer W. Automata-based refinement checking for real-time systems. Computer Science-Research and Development, 2015, 30(3): 255–283. [doi: 10.1007/s00450-014-0257-9]
    [28] UPPAAL. 2022. https://uppaal.org/
    [29] Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235. [doi: 10.1016/0304-3975(94)90010-8]
    [30] Clarke EM, Henzinger TA, Veith H, Bloem R. Handbook of Model Checking. Berlin: Springer, 2018. 1001–1046.
    [31] Alur R, Courcoubetis C, Henzinger TA. The observational power of clocks. In: Proc. of the 5th Int’l Conf. on Concurrency Theory. Uppsala: Springer, 1994. 162–177.
    [32] Kocher PC. Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Proc. of the 16th Annual Int’l Cryptology Conf. Santa Barbara: Springer, 1996. 104–113.
    [33] RSA Laboratories. RSAREF. 2016. https://sourceforge.net/projects/rsaref/
    [34] McLean J. A general theory of composition for trace sets closed under selective interleaving functions. In: Proc. of the 1994 IEEE Computer Society Symp. on Research in Security and Privacy. Oakland: IEEE, 1994. 79–93.
    [35] Lattner C, Adve V. LLVM: A compilation framework for lifelong program analysis & transformation. In: Proc. of the 2008 Int’l Symp. on Code Generation and Optimization. Piscataway: IEEE, 2008. 1–20.
    [36] Eclipse papyrusTM modeling environment. 2023. https://www.eclipse.org/papyrus/
    [37] 石正璞, 崔敏, 谢果君, 陈钢. 多旋翼飞控推进子系统的Coq形式化验证. 软件学报, 2022, 33(6): 2150-2171. http://www.jos.org.cn/1000-9825/6575.htm
    Shi ZP, Cui M, Xie GJ, Chen G. Coq formalization of propulsion subsystem of flight control system for multicopter. Ruan Jian Xue Bao/Journal of Software, 2022, 33(6): 2150–2171 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

刘乔森,孙聪,魏晓敏,曾荟铭,马建峰.多时间无干扰性验证方法.软件学报,2024,35(10):4729-4750

Copy
Share
Article Metrics
  • Abstract:378
  • PDF: 1699
  • HTML: 571
  • Cited by: 0
History
  • Received:September 29,2022
  • Revised:March 28,2023
  • Online: November 15,2023
  • Published: October 06,2024
You are the first2032315Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063