微信服务号

微信订阅号

2025年3月14日 20:28 星期五
首页 > 过刊浏览>2023年第34卷第8期 >3527-3548. DOI:10.13328/j.cnki.jos.006869
PDF HTML阅读 XML下载 导出引用 引用提醒
L4虚拟内存子系统的形式化验证
作者:
作者简介:

章乐平(1994-),男,博士生,主要研究领域为形式化方法,自动化验证,信息流安全;李悦欣(1998-),女,硕士生,主要研究领域为形式化方法,程序验证;赵永望(1979-),男,博士,教授,博士生导师,CCF杰出会员,主要研究领域为形式化方法,操作系统内核及安全,编程语言,安全攸关系统与软件,模型学习与程序合成;冯潇潇(1997-),男,硕士生,主要研究领域为形式化方法,操作系统设计;王布阳(1996-),男,硕士生,主要研究领域为形式化验证.

通讯作者:

赵永望,E-mail:zhaoyw@zju.edu.cn

基金项目:

国家自然科学基金（62132014）；浙江省尖兵计划（2022C01045）


Formal Verification of Virtual Memory Subsystem in L4
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [44]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足，这引起学术界和工业界的关注.内核是实现操作系统的基础组件，一旦出现错误，可能导致整个系统瘫痪，进一步对用户造成损失.因此，提高内核的正确性和可靠性至关重要.虚拟内存子系统是实现L4内核的关键机制，聚焦于对该机制进行形式建模和验证.构建了L4虚拟内存子系统的形式模型，该模型涉及映射机制所有操作、地址空间所有管理操作以及带TLB的MMU行为等；形式化了功能正确性、功能安全和信息安全三方面的属性；通过部分正确性、不变式以及展开条件的推理，在定理证明器Isabelle/HOL中证明了提出的形式模型满足这些属性.在建模和验证过程中，发现源代码在功能正确性和信息安全方面共存在3点问题，给出了相应的解决方案或建议.

    Abstract:

    L4, the second-generation of microkernel, greatly compensates for the shortcomings of the first-generation of microkernel in flexibility and performance, which has attracted the attention of academia and industry. The kernel is the basic component for implementing the operating system. Once it has errors, it may cause the breakdown of whole system, further causing losses to users. Therefore, it is very important to improve the correctness and reliability of the kernel. Virtual memory subsystem is a key mechanism to implement L4 kernel. This study focuses on the formal modeling and verification of this mechanism. A formal model is presented, which involves all operations of mapping mechanism, all management operations of address space, and MMU behavior with TLB. The properties of functional correctness, safety, and security are formalized. Through reasoning about partial correctness, invariants and unwinding conditions, it is shown that the proposed model satisfies these properties in the theorem prover Isabelle/HOL. During modeling and verification, three problems are found related to functional correctness and security in source code. The corresponding solutions or suggestions are given in this study as well.

    参考文献
    [1] Liedtke J.On micro-kernel construction.ACM SIGOPS Operating Systems Review, 1995, 29(5):237-250.[doi:10.1145/224057.224075]
    [2] Liedtke J.Towards real microkernels.Communications of the ACM, 1996, 30(9):70-77.[doi:10.1145/234215.234473]
    [3] L4Ka Team.L4 eXperimental kernel reference manual version X.2.2011.https://www.l4ka.org/l4ka/l4-x2-r7.pdf
    [4] Accetta MJ, Baron RV, Bolosky WJ, et al.Mach:A new kernel foundation for UNIX development.In:Proc.of the USENIX Summer Conf.USENIX Association, 1986.93-113.
    [5] Heiser G, Elphinstone K.L4 microkernels:The lessons from 20 years of research and deployment.ACM Trans.on Computer Systems (TOCS), 2016, 34(1):1-29.[doi:10.1145/2893177]
    [6] Elphinstone K, Heiser G.From L3 to seL4 what have we learnt in 20 years of L4 microkernels? In:Proc.of the 24th ACM Symp.on Operating Systems Principles (SOSP).ACM, 2013.133-150.[doi:10.1145/2517349.2522720]
    [7] Härtig H, Hohmuth M, Liedtke J, et al.The performance of m-kernel-based systems.In:Proc.of the 16th ACM Symp.on Operating System Principles (SOSP).ACM, 1997.66-77.[doi:10.1145/268998.266660]
    [8] Lackorzynski A, Warg A.Taming subsystems:Capabilities as universal resource access control in L4.In:Proc.of the 2nd Workshop on Isolation and Integration in Embedded Systems.ACM, 2009.25-30.[doi:10.1145/1519130.1519135]
    [9] Tuch H, Klein G.Verifying the L4 virtual memory subsystem.In:Proc.of the NICTA Formal Methods Workshop on Operating Systems Verification.National ICT Australia, 2004.73-97.
    [10] Klein G, Tuch H.Towards Verified Virtual Memory in L4.TPHOLs Emerging Trends, 2004.
    [11] Saraswat VA, Jagadeesan R, Michael MM, et al.A theory of memory models.In:Proc.of the 12th ACM SIGPLAN Symp.on Principles and Practice of Parallel Programming (PPoPP).ACM, 2007.161-172.[doi:10.1145/1229428.1229469]
    [12] Leroy X, Blazy S.Formal verification of a C-like memory model and its uses for verifying program transformations.Journal of Automated Reasoning, 2008, 41(1):1-31.[doi:10.1007/s10817-008-9099-0]
    [13] Gallardo MM, Merino P, Sanán D.Model checking dynamic memory allocation in operating systems.Journal of Automated Reasoning, 2009, 42(2):229-264.[doi:10.1007/s10817-009-9124-y]
    [14] Mansky W, Garbuzov D, Zdancewic S.An axiomatic specification for sequential memory models.In:Proc.of the 27th Int'l Conf.on Computer Aided Verification.Cham:Springer, 2015.413-428.[doi:10.1007/978-3-319-21668-3_24]
    [15] Ševčík J, Vafeiadis V, Nardelli FZ, et al.CompCertTSO:A verified compiler for relaxed-memory concurrency.Journal of the ACM (JACM), 2013, 60(3):1-50.[doi:10.1145/2487241.2487248]
    [16] Tews H, Völp M, Weber T.Formal memory models for the verification of low-level operating-system code.Journal of Automated Reasoning, 2009, 42(2):189-227.[doi:10.1007/s10817-009-9122-0]
    [17] Vaynberg A, Shao Z.Compositional verification of a baby virtual memory manager.In:Proc.of the 2nd Int'l Conf.on Certified Programs and Proofs (CPP).Berlin, Heidelberg:Springer, 2012.143-159.[doi:10.1007/978-3-642-35308-6_13]
    [18] Alkassar E, Schirmer N, Starostin A.Formal pervasive verification of a paging mechanism.In:Proc.of the 14th Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).Berlin, Heidelberg:Springer, 2008.109-123.[doi:10.1007/978-3-540-78800-3_9]
    [19] Blanchard A, Kosmatov N, Lemerre M, et al.A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C.In:Proc.of the 20th Int'l Workshop on Formal Methods for Industrial Critical Systems (FMICS).Cham:Springer, 2015.15-30.[doi:10.1007/978-3-319-19458-5_2]
    [20] Bolignano P, Jensen T, Siles V.Modeling and abstraction of memory management in a hypervisor.In:Proc.of the 19th Int'l Conf.on Fundamental Approaches to Software Engineering (FASE).Berlin, Heidelberg:Springer, 2016.214-230.[doi:10.1007/978-3-662-49665-7_13]
    [21] Zhao Y, Sanán D.Rely-guarantee reasoning about concurrent memory management in zephyr RTOS.In:Proc.of the 31st Int'l Conf.on Computer Aided Verification (CAV).Cham:Springer, 2019.515-533.[doi:10.1007/978-3-030-25543-5_29]
    [22] L4Ka Team.L4 pistachio source code, release version 0.4.2022.https://www.l4ka.org/154.php
    [23] Nipkow T, Paulson LC, Wenzel M.Isabelle/HOL:A Proof Assistant for Higher-order Logic.Springer Science & Business Media, 2002.[doi:10.1007/3-540-45949-9]
    [24] Klein G, Norrish M, Sewell T, et al.seL4:Formal verification of an OS kernel.In:Proc.of the 22nd ACM SIGOPS Symp.on Operating Systems Principles (SOSP).Montana:ACM, 2009.207-220.[doi:10.1145/1629575.1629596]
    [25] Gu R, Shao Z, Chen H, et al.CertiKOS:An extensible architecture for building certified concurrent OS kernels.In:Proc.of the 12th USENIX Symp.on Operating Systems Design and Implementation (OSDI).Savannah:USENIX Association, 2016.653-669.
    [26] Fang B, Sighireanu M.Hierarchical shape abstraction for analysis of free list memory allocators.In:Proc.of the 26th Int'l Symp.on Logic-based Program Synthesis and Transformation (LOPSTR).Cham:Springer, 2016.151-167.[doi:10.1007/978-3-319-63139-4_9]
    [27] Fang B, Sighireanu M.A refinement hierarchy for free list memory allocators.In:Proc.of the 2017 ACM SIGPLAN Int'l Symp.on Memory Management (ISMM).ACM, 2017.104-114.[doi:10.1145/3092255.3092275]
    [28] Fang B, Sighireanu M, Pu G, et al.Formal modelling of list based dynamic memory allocators.Science China Information Sciences, 2018, 61(12):1-16.[doi:10.1007/s11432-017-9280-9]
    [29] Marti N, Affeldt R, Yonezawa A.Formal verification of the heap manager of an operating system using separation logic.In:Proc.of the 8th Int'l Conf.on Formal Engineering Methods (ICFEM).Berlin, Heidelberg:Springer, 2006.400-419.[doi:10.1007/11901433_22]
    [30] Su W, Abrial JR, Pu G, et al.Formal development of a real-time operating system memory manager.In:Proc.of the 20th Int'l Conf.on Engineering of Complex Computer Systems (ICECCS).IEEE, 2015.130-139.[doi:10.1109/ICECCS.2015.24]
    [31] Yu D, Hamid NA, Shao Z.Building certified libraries for PCC:Dynamic storage allocation.In:Proc.of the 12th European Symp.on Programming (ESOP).Berlin, Heidelberg:Springer, 2003.363-379.[doi:10.1007/3-540-36575-3_25]
    [32] Rushby J.Noninterference, Transitivity, and Channel-control Security Policies.Menlo Park:SRI Int'l, Computer Science Laboratory, 1992.
    [33] 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]
    [34] Von Oheimb D.Information flow control revisited:Noninfluence=noninterference+nonleakage.In:Proc.of the 2004 European Symp.on Research in Computer Security (ESORICS).Berlin:Springer, 2004.225-243.[doi:10.1007/978-3-540-30108-0_14]
    [35] Murray T, Matichuk D, Brassil M, et al.Noninterference for operating system kernels.In:Proc.of the 2nd Int'l Conf.on Certified Programs and Proofs (CPP).Berlin, Heidelberg:Springer, 2012.126-142.[doi:10.1007/978-3-642-35308-6_12]
    [36] Murray T, Matichuk D, Brassil M, et al.seL4:From general purpose to a proof of information flow enforcement.In:Proc.of the 2013 IEEE Symp.on Security and Privacy (S&P).IEEE Computer Society, 2013.415-429.[doi:10.1109/SP.2013.35]
    [37] Costanzo D, Shao Z, Gu R.End-to-end verification of information-flow security for C and assembly programs.In:Proc.of the 37th ACM SIGPLAN Conf.on Programming Language Design and Implementation (PLDI).ACM, 2016.648-664.[doi:10.1145/2908080.2908100]
    [38] Sigurbjarnarson H, Nelson L, Castro-Karney B, et al.Nickel:A framework for design and verification of information flow control systems.In:Proc.of the 13th USENIX Symp.on Operating Systems Design and Implementation (OSDI).2018.287-305.
    [39] Zhao Y, Sanán D, Zhang F, et al.Reasoning about information flow security of separation kernels with channel-based communication.In:Proc.of the 22nd Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).Berlin, Heidelberg:Springer, 2016.791-810.[doi:10.1007/978-3-662-49674-9_50]
    [40] Zhao Y, Sanán D, Zhang F, et al.Refinement-based specification and security analysis of separation kernels.IEEE Trans.on Dependable and Secure Computing, 2017, 16(1):127-141.[doi:10.1109/TDSC.2017.2672983]
    [41] Hawblitzel C, Howell J, Lorch JR, et al.Ironclad apps:End-to-end security via automated full-system verification.In:Proc.of the 11th USENIX Symp.on Operating Systems Design and Implementation (OSDI).USENIX Association, 2014.165-181.
    [42] Syeda HT, Klein G.Program verification in the presence of cached address translation.In:Proc.of the 9th Int'l Conf.on Interactive Theorem Proving (ITP).Cham:Springer, 2018.542-559.[doi:10.1007/978-3-319-94821-8_32]
    [43] Hoare CAR.An axiomatic basis for computer programming.Communications of the ACM, 1969, 12(10):576-580.[doi:10.1145/363235.363259]
    [44] Wenzel M.The Isabelle/Isar reference manual.2021.http://isabelle.in.tum.de/doc/isar-ref.pdf
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

章乐平,赵永望,王布阳,李悦欣,冯潇潇. L4虚拟内存子系统的形式化验证.软件学报,2023,34(8):3527-3548

复制
分享
文章指标
  • 点击次数:1237
  • 下载次数: 3836
  • HTML阅读次数: 2737
  • 引用次数: 0
历史
  • 收稿日期:2022-09-05
  • 最后修改日期:2022-10-13
  • 在线发布日期: 2022-12-30
  • 出版日期: 2023-08-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19700975位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号