Computer Science ›› 2019, Vol. 46 ›› Issue (3): 170-179.doi: 10.11896/j.issn.1002-137X.2019.03.026
• Information Security • Previous Articles Next Articles
CHEN Hao, LUO Lei, LI Yun, CHEN Li-rong
CLC Number:
| [1]SMITH J,NAIR R.Virtual machines:versatile platforms for systems and processes[M].San Francisco,California,USA:Elsevier,2005. [2]SHU R,WANG P,GORSKI S A,et al.A Study of Security Isolation Techniques[J].ACM Computing Surveys,2016,49(3):1-37. [3]CHONG S,GUTTMAN J,DATTA A,et al.Report on the NSF Workshop on Formal Methods for Security[R].College Park,MD,USA:National Science Foundation,2016. [4]SCHMITTNER C,MA Z.Towards a Framework for Alignment Between Automotive Safety and Security Standards[C]∥Computer Safety,Reliability,and Security:SAFECOMP 2015 Workshops.Cham,Netherlands:Springer International Publishing,2015:133-143. [5]BECKER H,CRESPO J M,GALOWICZ J,et al.Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor[C]∥International Symposium on Formal Methods.Limassol,Cyprus:Springer,Cham,2016:69-84. [6]MATICHUK D,MURRAY T,ANDRONICK J,et al.Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification[C]∥Proceedings of the 37th International Confe-rence on Software Engineering-Volume 1.Piscataway,NJ,USA:IEEE Press,2015:722-732. [7]WU C,WANG Z,JIANG X.Taming hosted hypervisors with (mostly) deprivileged execution[C]∥Proceedings of the Network and Distributed System Security Symposium (NDSS).San Diego,CA,USA:Internet Society,2013:1-15. [8]PAN W,ZHANG Y,YU M,et al.Improving Virtualization Security by Splitting Hypervisor into Smaller Components[C]∥Proceedings of the 26th Annual IFIP WG 11.3 Conference on Data and Applications Security and Privacy.Berlin,Heidelberg:Springer-Verlag,2012:298-313. [9]SANN D,BUTTERFIELD A,HINCHEY M.Separation Ker- nel Verification:The Xtratum Case Study[C]∥Working Conference on Verified Software:Theories,Tools,and Experiments.Vienna,Austria:Springer,Cham,2014:133-149. [10]PENNEMAN N,KUDINSKAS D,RAWSTHORNE A,et al. Formal virtualization requirements for the ARM architecture[J].Journal of Systems Architecture,2013,59(3):144-154. [11]BARTHE G,BETARTE G,CAMPO J D,et al.Formally Verified Implementation of an Idealized Model of Virtualization[C]∥19th International Conference on Types for Proofs and Programs (TYPES 2013).Dagstuhl,Germany:Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,2014:45-63. [12]NEMATI H,GUANCIALE R,DAM M.Trustworthy Virtuali- zation of the ARMv7 Memory Subsystem[C]∥International Conference on Current Trends in Theory and Practice of Informatics.Berlin:Springer,2015:578-589. [13]BLANCHARD A,KOSMATOV N,LEMERRE M,et al.A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C[C]∥International Workshop on Formal Methods for Industrial Critical Systems.Berlin:Springer,2015:15-30. [14]BAUMANN C,SCHWARZ O,DAM M.Compositional Verification of Security Properties for Embedded Execution Platforms[C]∥6th International Workshop on Security Proofs for Embedded Systems(PROOFS 2017).Taipei,Taiwan,China,EPiC open access,2017:1-16. [15]NORDHOLZ J.Design and provability of a statically configurable hypervisor[D].Berlin:Technische Universitt Berlin,2017. [16]LEINENBACH D,SANTEN T.Verifying the Microsoft Hyper-V Hypervisor with VCC[C]∥Proceedings of the 2Nd World Congress on Formal Methods.Berlin,Heidelberg:Springer-Verlag,2009:806-809. [17]ALKASSAR E,HILLEBRAND M A,PAUL W J,et al.Automated Verification of a Small Hypervisor[C]∥Proceedings of the Third International Conference on Verified Software:Theories,Tools,Experiments.Berlin,Heidelberg:Springer-Verlag,2010:40-54. [18]KLEIN G,ANDRONICK J,ELPHINSTONE K,et al.Comprehensive Formal Verification of an OS Microkernel[J].ACM Transactions on Computer Systems,2014,32(1):2:1-2:70. [19]VASUDEVAN A,CHAKI S,JIA L,et al.Design,Implementation and Verification of an eXtensible and Modular Hypervisor Framework[C]∥2013 IEEE Symposium on Security and Privacy.Berkeley,CA,USA:IEEE Press,2013:430-444. [20]BOLIGNANO P.Formal models and verification of memory management in a hypervisor[D].Breizh:Université Rennes 1,2017. [21]BARTHE G,BETARTE G,CAMPO J D,et al.Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization[C]∥2012 IEEE 25th Computer Security Foundations Symposium.Cambridge,MA,USA:IEEE Press,2012:186-197. [22]BOLIGNANO P,JENSEN T,SILES V.Modeling and Abstraction of Memory Management in a Hypervisor[C]∥International Conference on Fundamental Approaches to Software Engineering.Berlin,Germany:Springer,2016:214-230. [23]KOVALEV M.TLB virtualization in the context of hypervisor verification[D].Saarbrucken:Saarland University,2013. [24]MOGOSANU L,CARABAS M,CONDURACHE C,et al.Eva- luating Architecture-Dependent Linux Performance[C]∥2015 20th International Conference on Control Systems and Computer Science.New York:IEEE Press,2015:499-505. [25]ABDELRAHEM O,BAHAA-ELDIN A M,TAHA A.Virtuali- zation security:A survey[C]∥2016 11th International Conferen-ce on Computer Engineering Systems (ICCES).Cairo,Egypt:IEEE Press,2016:32-40. [26]FENG X,SHAO Z,GUO Y,et al.Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems[C]∥Proceedings of the 2Nd International Conference on Verified Software:Theories,Tools,Experiments.Berlin,Heidelberg:Springer-Verlag,2008:54-69. [27]GU R,KOENIG J,RAMANANANDRO T,et al.Deep Specifications and Certified Abstraction Layers[C]∥Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.New York,NY,USA:ACM,2015:595-608. [28]BERTOT Y,HUET G,CASTRAN P,et al.Interactive Theorem Proving and Program Development:Coq’Art:The Calculus of Inductive Constructions[M].Berlin,Germany:Springer Berlin Heidelberg,2013:1-472. [29]HEISER G.The Role of Virtualization in Embedded Systems[C]∥Proceedings of the 1st Workshop on Isolation and Integration in Embedded Systems.New York,NY,USA:ACM,2008:11-16. [30]GE Q,YAROM Y,COCK D,et al.A survey of microarchitectural timing attacks and countermeasures on contemporary hardware[J].Journal of Cryptographic Engineering,2018,8(1):1-27. [31]KIM J H,LEE S H,JIN H W.Supporting Virtualization Stan- dard for Network Devices in RTEMS Real-time Operating System[J].ACM SIGBED Review,2016,13(1):35-40. [32]KLEIN G.Operating system verification—An overview[J]. Sadhana,2009,34(1):27-69. [33]LEROY X,BLAZY S,KSTNER D,et al.CompCert-A Formally Verified Optimizing Compiler[C]∥ERTS 2016:Embedded Real Time Software and Systems,8th European Congress.Toulouse,France:SEE,2016. [34]LEROY X,BLAZY S.Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations[J].Journal of Automated Reasoning,2008,41(1):1-31. [35]STAELIN C.Lmbench:an extensible micro-benchmark suite [J].Software:Practice and Experience,2005,35(11):1079-1105. [36]KLEINERT B,WEI S,SCHFER F,et al.Adaptive Synchronization Interface for Hardware-Software Co-Simulation Based on SystemC and QEMU[C]∥Proceedings of the 9th EAI International Conference on Simulation Tools and Techniques.ICST,Brussels,Belgium,Belgium:ICST,2016:28-36. [37]DESHPANDE S M,AINAPURE B.An Intelligent Virtual Machine Monitoring System Using KVM for Reliable And Secure Environment in Cloud[C]∥2016 IEEE International Conference on Advances in Electronics,Communication and Computer Technology (ICAECCT).New York:IEEE Press,2016:314-319. [38]PU J,SONG Z,TILEVICH E.Understanding the Energy,Performance,and Programming Effort Trade-Offs of Android Persistence Frameworks[C]∥2016 IEEE 24th International Symposium on Modeling,Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS).London,United Kingdom:IEEE Press,2016:433-438. |
| [1] | JIAN Qi-rui, CHEN Ze-mao, WU Xiao-kang. Authentication and Key Agreement Protocol for UAV Communication [J]. Computer Science, 2022, 49(8): 306-313. |
| [2] | WANG Ran-ran, WANG Yong, CAI Yu-tong, JIANG Zheng-tao, DAI Gui-ping. Formal Verification of Yahalom Protocol Based on Process Algebra [J]. Computer Science, 2021, 48(6A): 481-484. |
| [3] | LI Ling, LI Huang-hua, WANG Sheng-yuan. Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design [J]. Computer Science, 2020, 47(6): 8-15. |
| [4] | FAN Yong-qian, CHEN Gang, CUI Min. Formalization of Finite Field GF(2n) Based on COQ [J]. Computer Science, 2020, 47(12): 311-318. |
| [5] | MA Zhen-wei,CHEN Gang. Matrix Formalization Based on Coq Record [J]. Computer Science, 2019, 46(7): 139-145. |
| [6] | TANG Hong-mei and ZHENG Gang. Design and Optimization on Virtual Desktop Infrastructure Based on KVM [J]. Computer Science, 2017, 44(Z6): 560-562. |
| [7] | LI Yan-chun, LI Xiao-juan, GUAN Yong, WANG Rui, ZHANG Jie and WEI Hong-xing. xMAS-based Formal Verification of SpaceWire Credit Logic [J]. Computer Science, 2016, 43(2): 113-117. |
| [8] | YANG Xiu-mei, GUAN Yong, SHI Zhi-ping, WU Ai-xuan, ZHANG Qian-ying and ZHANG Jie. Higher-order Logic Formalization of Function Matrix and its Calculus [J]. Computer Science, 2016, 43(11): 24-29. |
| [9] | CHEN Li-rong, LI Yun and LUO Lei. Research on Formal Verification of Embedded Operating System [J]. Computer Science, 2015, 42(8): 203-214. |
| [10] | LI Qing-bao, ZHANG Ping and ZENG Guang-yu. Integrity Based Security Protection Method for Terminal Computer [J]. Computer Science, 2015, 42(6): 162-166. |
| [11] | LIU Yang,YANG Fei,SHI Gang,YAN Xin,WANG Sheng-yuan and DONG Yuan. Brief Overview of Translation Validation Method in Trusted Compiler Construction [J]. Computer Science, 2014, 41(Z6): 334-338. |
| [12] | ZHOU Kuan-jiu,REN Long-tao,WANG Xiao-long,YONG Jia-wei and HOU Gang. Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix [J]. Computer Science, 2014, 41(8): 42-46. |
| [13] | LI Qian and YU Wen-sheng. Safety Verification for VCCR Subsystem of Space Life Support System [J]. Computer Science, 2014, 41(6): 193-198. |
| [14] | LI Min,LUO Hui-qiong,TANG Chun-ling and WANG Qiang. Research on Formal Verification of Web Interaction Model [J]. Computer Science, 2014, 41(2): 219-221. |
| [15] | HUANG Cong-hui,CHEN Jing,GONG Shui-qing and CHEN Ming-hua. Research of Method for Virtualizing 64-bit Windows Application Binary Interface [J]. Computer Science, 2014, 41(1): 39-42. |
|
||
Home