請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/100954完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 黎士瑋 | zh_TW |
| dc.contributor.advisor | Shih-Wei Li | en |
| dc.contributor.author | 鄭明淵 | zh_TW |
| dc.contributor.author | Beng Yen Teh | en |
| dc.date.accessioned | 2025-11-26T16:14:19Z | - |
| dc.date.available | 2025-11-27 | - |
| dc.date.copyright | 2025-11-26 | - |
| dc.date.issued | 2025 | - |
| dc.date.submitted | 2025-10-27 | - |
| dc.identifier.citation | [1] Apache http server benchmarking tool. http://httpd.apache.org/docs/2.4/programs/ab.html.
[2] Kernel module signing facility. https://www.kernel.org/doc/html/v4.18/admin-guide/module-signing.html. [3] Lifting the (hyper) visor:Bypassing samsung＇s real-time kernel protection. https://googleprojectzero.blogspot.com/2017/02/lifting-hyper-visor-bypassing-samsungs.html. [4] The Coq Proof Assistant. http://coq.inria.fr. [Accessed on Sep 6, 2025]. [5] Improve hackbench. http://people.redhat.com/mingo/cfs-scheduler/tools/hackbench.c, 2008. [6] Windows 8 kernel memory protections bypass. https://labs.withsecure.com/publications/windows-8-kernel-memory-protections-bypass, 2014. [7] arm64: entry: Hook up entry trampoline to exception vectors. https://patchwork.kernel.org/project/linux-arm-kernel/patch/1512059986-21325-14-git-send-email-will.deacon@arm.com/, 2017. [8] Virtualization based security. https://learn.microsoft.com/en-us/windows-hardware/design/device-experiences/oem-vbs, 2023. [9] 7-CPU.COM. Applied micro x-gene. https://www.7-cpu.com/cpu/X-Gene.html [Accessed: Apr 28, 2021]. [10] A. M. Azab, P. Ning, J. Shah, Q. Chen, R. Bhutkar, G. Ganesh, J. Ma, and W. Shen. Hypervision across worlds: Real-time kernel protection from the arm trustzone secure world. In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pages 90–102, 2014. [11] P. Barham, B. Dragovic, K. Fraser, S. Hand, T. Harris, A. Ho, R. Neugebauer, I. Pratt, and A. Warfield. Xen and the Art of Virtualization. In Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP 2003), pages 164–177, Bolton Landing, NY, Oct. 2003. [12] M. Brun, R. Achermann, T. Chajed, J. Howell, G. Zellweger, and A. Lattuada. Beyond isolation: Os verification as a foundation for correct applications. In Proceedings of the 19th Workshop on Hot Topics in Operating Systems, pages 158–165, 2023. [13] C. Cadar, D. Dunbar, D. R. Engler, et al. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, volume 8, pages 209–224, 2008. [14] D. Calavera and L. Fontana. Linux Observability with BPF: Advanced Programming for Performance Analysis and Networking. O’Reilly Media, 2019. [15] C. Castes, F. Costa, N. Foster, T. Bourgeat, and E. Bugnion. Lightweight hypervisor verification: Putting the hardware burger on a diet. In Proceedings of the 2025 Workshop on Hot Topics in Operating Systems, pages 27–33, 2025. [16] C. Cebeci, Y. Zou, D. Zhou, G. Candea, and C. Pit-Claudel. Practical verification of system-software components written in standard c. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, pages 455–472, 2024. [17] X. Chen, Z. Li, L. Mesicek, V. Narayanan, and A. Burtsev. Atmosphere: Towards practical verified kernels in rust. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification, pages 9–17, 2023. [18] E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. Vcc: A practical system for verifying concurrent c. In International Conference on Theorem Proving in Higher Order Logics, pages 23–42. Springer, 2009. [19] Columbia University. OSDI 23: Artifact Evaluation: Spoq: Scaling Machine-Checkable Systems Verification in Coq. https://github.com/columbia/osdi23-paper114-ae, Sept. 2021. [20] B. F. Cooper, A. Silberstein, E. Tam, R. Ramakrishnan, and R. Sears. Benchmarking cloud serving systems with ycsb. In Proceedings of the 1st ACM symposium on Cloud computing, pages 143–154, 2010. [21] J. Corbet. The current state of kernel page-table isolation. https://lwn.net/Articles/741878/, Dec. 2017. [22] J. Corbet. Kernel support for hardware-based control-flow integrity. https://lwn.net/Articles/900099/, July 2022. [23] J. Corbet. Shadow stacks for 64-bit Arm systems. https://lwn.net/Articles/940403/, Aug. 2023. [24] Z. Dai, S. Liu, V. Sjoberg, X. Li, Y. Chen, W. Wang, Y. Jia, S. N. Anderson, L. Elbeheiry, S. Sondhi, et al. Verifying rust implementation of page tables in a software enclave hypervisor. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2, pages 1218–1232, 2024. [25] L. De Moura and N. Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008. [26] A. Ferraiuolo, A. Baumann, C. Hawblitzel, and B. Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th Symposium on Operating Systems Principles, pages 287–305, 2017. [27] S. Fischer. Supervisor mode execution protection. In NSA Trusted Computing Conference, 2011. [28] X. Ge and T. Jaeger. Sprobes: Enforcing kernel code integrity on the TrustZone architecture. In Proceedings of the Mobile Security Technologies 2014 Workshop, 2014. [29] X. Ge, N. Talele, M. Payer, and T. Jaeger. Fine-grained control-flow integrity for kernel software. In 2016 IEEE European Symposium on Security and Privacy (EuroS&P), pages 179–194, 2016. [30] R. Gu, Z. Shao, H. Chen, J. Kim, J. Koenig, X. Wu, V. Sjöberg, and D. Costanzo. Building certified concurrent os kernels. Communications of the ACM, 62(10):89–99, 2019. [31] R. Gu, Z. Shao, H. Chen, X. N. Wu, J. Kim, V. Sjöberg, and D. Costanzo. {CertiKOS}: An extensible architecture for building certified concurrent {OS} kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), pages 653–669, 2016. [32] R. Gu, Z. Shao, J. Kim, X. Wu, J. Koenig, V. Sjöberg, H. Chen, D. Costanzo, and T. Ramananandro. Certified concurrent abstraction layers. ACM SIGPLAN Notices, 53(4):646–661, 2018. [33] O. S. Hofmann, A. M. Dunn, S. Kim, I. Roy, and E. Witchel. Ensuring operating system kernel integrity with osck. SIGARCH Comput. Archit. News, 39(1):279–290, mar 2011. [34] B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for c and java. In NASA formal methods symposium, pages 41–55. Springer, 2011. [35] X. Jiang, X. Wang, and D. Xu. Stealthy malware detection through vmm-based out-of-the-box＇semantic view. In 14th ACM Conference on Computer and Communications Security (CCS), Alexandria, VA (November 2007), volume 10, 2007. [36] R. Jones. Netperf. https://github.com/HewlettPackard/netperf, Accessed 2025. [37] V. P. Kemerlis, G. Portokalidis, and A. D. Keromytis. kGuard: Lightweight kernel protection against Return-to-User attacks. In 21st USENIX Security Symposium (USENIX Security 12), pages 459–474, Bellevue, WA, Aug. 2012. USENIX Association. [38] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207–220, 2009. [39] I. Korkin. Hypervisor-based active data protection for integrity and confidentiality of dynamically allocated memory in windows kernel. arXiv preprint arXiv:1805.11847, 2018. [40] R. Labs. Memtier benchmark. https://github.com/RedisLabs/memtier_benchmark, Accessed 2025. [41] J. Lee, H. Ham, I. Kim, and J. Song. Poster: Page table manipulation attack. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, pages 1644–1646, 2015. [42] D. Leinenbach and T. Santen. Verifying the microsoft hyper-v hypervisor with vcc. In International Symposium on Formal Methods, pages 806–809. Springer, 2009. [43] K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning, pages 348–370. Springer, 2010. [44] X. Leroy, S. Blazy, D. Kästner, B. Schommer, M. Pister, and C. Ferdinand. Compcert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, 2016. [45] J. LI. K-Int, Kernel Code Integrity Enforcer. Master’s thesis, National Taiwan University, June 2023. [46] J. Li, S. Miller, D. Zhuo, A. Chen, J. Howell, and T. Anderson. An incremental path towards a safer os kernel. In Proceedings of the Workshop on Hot Topics in Operating Systems, HotOS ’21, page 183–190, New York, NY, USA, 2021. Association for Computing Machinery. [47] S.-W. Li, X. Li, R. Gu, J. Nieh, and J. Z. Hui. A Secure and Formally Verified Linux KVM Hypervisor. In Proceedings of the 2021 IEEE Symposium on Security and Privacy (IEEE S&P 2021), May 2021. [48] S.-W. Li, X. Li, R. Gu, J. Nieh, and J. Z. Hui. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. In Proceedings of the 30th USENIX Security Symposium (USENIX Security 2021), Aug. 2021. [49] X. Li, X. Li, C. Dall, R. Gu, J. Nieh, Y. Sait, and G. Stockwell. Design and verification of the arm confidential compute architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22), pages 465–484, 2022. [50] X. Li, X. Li, W. Qiang, R. Gu, and J. Nieh. Spoq: Scaling Machine-Checkable systems verification in coq. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23), pages 851–869, Boston, MA, July 2023. USENIX Association. [51] D. P. McKee, Y. Giannaris, C. Ortega, H. Shrobe, M. Payer, H. Okhravi, and N. Burow. Preventing kernel hacks with hakcs. Proceedings 2022 Network and Distributed System Security Symposium, 2022. [52] V. Narayanan, Y. Huang, G. Tan, T. Jaeger, and A. Burtsev. Lightweight kernel isolation with virtualization and vm functions. In Proceedings of the 16th ACM SIGPLAN/SIGOPS international conference on virtual execution environments, pages 157–171, 2020. [53] National Taiwan University. ACSAC 24: Artifact Evaluation: SECvma: Virtualization-based Linux Kernel Protection for Arm. https://github.com/ae-acsac24-44/acsac24-paper240-ae, Dec. 2024. [54] L. Nelson, H. Sigurbjarnarson, K. Zhang, D. Johnson, J. Bornholt, E. Torlak, and X. Wang. Hyperkernel: Push-button verification of an os kernel. In Proceedings of the 26th Symposium on Operating Systems Principles, pages 252–269, 2017. [55] R. Nikolaev and G. Back. Virtuos: An operating system with kernel virtualization. In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, pages 116–132, 2013. [56] T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. [57] N. L. Petroni Jr and M. Hicks. Automated detection of persistent kernel control-flow attacks. In Proceedings of the 14th ACM conference on Computer and communications security, pages 103–115, 2007. [58] R. Riley, X. Jiang, and D. Xu. Guest-transparent prevention of kernel rootkits with vmm-based memory shadowing. In International Workshop on Recent Advances in Intrusion Detection, pages 1–20. Springer, 2008. [59] M. Salaün. Hypervisor-enforced kernel integrity (heki) for kvm. In Linux Plumbers Conference, 2023. [60] M. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, and D. Garg. Refinedc: automating the foundational verification of c code with refined ownership types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 158–174, 2021. [61] SAMSUNG. Real-time kernel protection (rkp), July 2023. https://docs.samsungknox.com/admin/fundamentals/whitepaper/core-platform-security/real-time-kernel-protection/. [62] SAMSUNG. Samsung knox | secure mobile platforms and solutions, 2023. https://www.samsungknox.com/. [63] A. Seshadri, M. Luk, N. Qu, and A. Perrig. Secvisor: A tiny hypervisor to provide lifetime kernel code integrity for commodity oses. In Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles, pages 335–350, 2007. [64] G. Strongin. Trusted computing using amd“pacifica＂and“presidio＂secure virtual machine technology. Information Security Technical Report, 10(2):120–132, 2005. [65] N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, et al. Dependent types and multi-monadic effects in f. In Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 256–270, 2016. [66] R. Tao, J. Yao, X. Li, S.-W. Li, J. Nieh, and R. Gu. Formal verification of a multi-processor hypervisor on arm relaxed memory hardware. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, SOSP ’21, page 866–881, New York, NY, USA, 2021. Association for Computing Machinery. [67] D. Tian, R. Ma, X. Jia, and C. Hu. A kernel rootkit detection approach based on virtualization and machine learning. IEEE Access, 7:91657–91666, 2019. [68] R. Uhlig, G. Neiger, D. Rodgers, A. L. Santoni, F. C. Martins, A. V. Anderson, S. M. Bennett, A. Kagi, F. H. Leung, and L. Smith. Intel virtualization technology. Computer, 38(5):48–56, 2005. [69] P. Varanasi and G. Heiser. Hardware-supported virtualization on arm. In Proceedings of the Second Asia-Pacific Workshop on Systems, pages 1–5, 2011. [70] X. Wang, J. Zhang, A. Zhang, and J. Ren. Tkrd: Trusted kernel rootkit detection for cybersecurity of vms based on machine learning and memory forensic analysis. Mathematical Biosciences and Engineering, 16(4):2650–2667, 2019. [71] X. Xiong, D. Tian, P. Liu, et al. Practical protection of kernel integrity for commodity os from untrusted extensions. In NDSS, volume 11, 2011. [72] F. Xu, M. Fu, X. Feng, X. Zhang, H. Zhang, and Z. Li. A practical verification framework for preemptive os kernels. In International Conference on Computer Aided Verification, pages 59–79. Springer, 2016. [73] T. B. Yen, J. Li, and S.-W. Li. Secvma: Virtualization-based linux kernel protection for arm. In 2024 Annual Computer Security Applications Conference (ACSAC), pages 579–592, 2024. [74] J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche. Hacl*: A verified modern cryptographic library. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pages 1789–1806, 2017. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/100954 | - |
| dc.description.abstract | 隨着單體式核心如 Linux 的規模與複雜度的不斷提升，其不僅造成了巨大的攻擊面，也引發了頻繁的安全性漏洞。雖然基於虛擬化的核心防護機制能透過硬體強制隔離提供強大的安全性，但它往往會帶來顯著的效能開銷，且僅僅是將信任邊界轉移到管理程式 (Hypervisor)。本論文提出 vSECvma，這是首個針對 Arm 架構、具備高效能且經過功能正確性形式化驗證的 Linux 核心防護框架。我們的工作證明了在強安全性、高效能與形式化保證之間能夠同時達成。在既有研究的基礎上，vSECvma 強化了安全性保證，並引入一系列新穎的最佳化技術，以緩解虛擬化方法所造成的效能負擔，從而維持 Linux 的效率與相容性。我們接著對系統核心進行功能正確性的形式化驗證。此驗證透過多重策略得以實現：重用來自SeKVM（經過形式化驗證的 KVM 管理程式）的已驗證元件；運用自動化驗證框架 Spoq；並將系統系統化地重構為更適合驗證的模型。本研究最終實現了首個能同時在 Arm 上提供強安全性與高效能，並具備功能正確性機器檢證證明的 Linux 核心防護框架。 | zh_TW |
| dc.description.abstract | Monolithic kernels such as Linux have grown vastly in complexity, creating a large attack surface with frequent vulnerabilities. While virtualization-based kernel protection offers strong, hardware-enforced isolation, it often incurs significant performance overhead and merely shifts the trust boundary to the hypervisor. This thesis presents vSECvma, the first high-performance Linux kernel protection framework on Arm to be formally verified for functional correctness. Our work demonstrates that it is possible to achieve strong security, high performance, and formal assurance simultaneously. Building on prior work, vSECvma strengthens security guarantees and incorporates a suite of novel optimizations to mitigate the performance overhead of virtualization-based approaches, thereby retaining Linux’s efficiency and compatibility. We then formally prove the functional correctness of its system’s core. Our verification is made tractable through a multi-faceted strategy: reusing verified components from the SeKVM, a formally verified KVM-based hypervisor; leveraging Spoq, an automated verification framework; and systematically restructuring the system into a verification-friendly model. Our work delivers the first framework for Linux on Arm that simultaneously achieves strong security and high performance, backed by a machine-checked proof of functional correctness. | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2025-11-26T16:14:19Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2025-11-26T16:14:19Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | 致謝 iii
摘要 v Abstract vii Contents ix List of Figures xi List of Tables xiii Chapter 1 Introduction 1 Chapter 2 Background 5 2.1 Formally Verified Systems . . . . . . . . . . . . . . . . . . . . . . .5 2.2 Spoq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 2.3 Introduction to K-Int . . . . . . . . . . . . . . . . . . . . . . . . . .10 Chapter 3 Threat Model And Assumptions 13 Chapter 4 Design 15 4.1 Security Enhancements . . . . . . . . . . . . . . . . . . . . . . . . .17 4.1.1 System Register Protection . . . . . . . . . . . . . . . . . . . . . .17 4.1.2 Supervisor Mode Execution Prevention . . . . . . . . . . . . . . .18 4.2 Optimization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .20 4.3 Adapting KPCore to Spoq Framework . . . . . . . . . . . . . . . . .23 4.3.1 Layered Design . . . . . . . . . . . . . . . . . . . . . . . . . . . .28 Chapter 5 Verifying Functional Correctness of KPCore 33 5.1 Abstract Machine Model Layer . . . . . . . . . . . . . . . . . . . .35 5.2 Functional Correctness of Page Tables . . . . . . . . . . . . . . . . .35 5.2.1 Stage 2 Page Table Management . . . . . . . . . . . . . . . . . . .36 5.2.2 Stage 1 Page Table Management . . . . . . . . . . . . . . . . . . .40 5.3 Functional Correctness of Secure Module Loading . . . . . . . . . .41 5.4 Ensured Invariants and Correctness Guarantees . . . . . . . . . . . .44 5.5 Addressing Limitations of Spoq . . . . . . . . . . . . . . . . . . . .46 Chapter 6 Evaluation 49 6.1 Performance Evaluation . . . . . . . . . . . . . . . . . . . . . . . .52 6.2 Bugs found in SECvma . . . . . . . . . . . . . . . . . . . . . . . . .56 Chapter 7 Related Work 61 Chapter 8 Limitations and Future Work 65 Chapter 9 Conclusion 67 References 69 | - |
| dc.language.iso | en | - |
| dc.subject | 作業系統 | - |
| dc.subject | 資訊安全 | - |
| dc.subject | 虛擬化 | - |
| dc.subject | 形式化驗證 | - |
| dc.subject | Operating Systems | - |
| dc.subject | Security | - |
| dc.subject | Virtualization | - |
| dc.subject | Formal Verification | - |
| dc.title | vSECvma：經優化與形式化驗證的 Arm 平台 Linux 核心保護框架 | zh_TW |
| dc.title | vSECvma: An Optimized and Formally Verified Linux Kernel Protection Framework on Arm | en |
| dc.type | Thesis | - |
| dc.date.schoolyear | 114-1 | - |
| dc.description.degree | 碩士 | - |
| dc.contributor.oralexamcommittee | 林忠緯;陳郁方;王超 | zh_TW |
| dc.contributor.oralexamcommittee | Chung-Wei Lin;Yu-Fang Chen;Chao Wang | en |
| dc.subject.keyword | 作業系統,資訊安全虛擬化形式化驗證 | zh_TW |
| dc.subject.keyword | Operating Systems,SecurityVirtualizationFormal Verification | en |
| dc.relation.page | 78 | - |
| dc.identifier.doi | 10.6342/NTU202504620 | - |
| dc.rights.note | 同意授權(全球公開) | - |
| dc.date.accepted | 2025-10-28 | - |
| dc.contributor.author-college | 電機資訊學院 | - |
| dc.contributor.author-dept | 資訊工程學系 | - |
| dc.date.embargo-lift | 2025-11-27 | - |
| 顯示於系所單位： | 資訊工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-114-1.pdf | 2.53 MB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。