微信服务号

微信订阅号

2025年5月10日 23:11 星期六
首页 > 过刊浏览>2015年第26卷第2期 >239-253. DOI:10.13328/j.cnki.jos.004778
PDF HTML阅读 XML下载 导出引用 引用提醒
设备驱动程序可靠性和正确性保障方法与技术研究进展
作者:
基金项目:

国家重点基础研究发展计划(973)(2014CB340703); 国家自然科学基金(91318301, 91118002, 61321491, 61402222); 教育部高等学校博士学科点专项科研基金(20110091120058); 江苏省产学研项目(BY2014126-03)


Research on Reliability and Correctness Assurance Methods and Techniques for Device Drivers
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [74]
    • |
  • 相似文献
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    随着计算机技术的不断发展,计算机系统在安全攸关领域得到了广泛应用,其中的软件系统正逐渐成为重要的使能部件.在计算机系统中,设备驱动程序扮演了软件与硬件设备之间桥梁的角色.由于与计算机平台、操作系统、设备3个方面同时关联所导致的复杂性,设备驱动程序的开发难度大、成本高,程序中所存在的错误和缺陷常常导致系统失效,在安全攸关领域造成不可挽回的损失.以设备驱动程序可靠性和正确性保障为目标,分别从故障的隔离与恢复、正确性分析和验证、设计建模与复杂性控制这3个方面对当前相关方法和技术进行分析,为开展进一步深入的研究工作打下基础.

    Abstract:

    With the rapid development of computer technology, computer systems have been widely used in the safety-critical field where software systems are important enabling components. In computer systems, device drivers act as the bridge between software and devices. Due to the complexity resulted from the fact that device drivers are associated with platforms, operating systems and devices all together, the development of device drivers is very difficult and costly. Errors and faults in device drivers often lead to system failures, causing irreparable damage to the safety-critical applications. Aiming at the assurance of reliability and correctness, the paper presents a survey of related methods and techniques from three aspects: failure isolation and recovery, correctness analysis and verification, model based design and complexity control. The mainstream methods and techniques are evaluated with their pros and cons, which lays the foundation for the further research.

    参考文献
    [1] Safety-Critical system. 1986. http://en.wikipedia.org/wiki/Life-critical_system
    [2] Device driver. 1968. http://en.wikipedia.org/wiki/Device_driver
    [3] Chou A, Yang J, Chelf B, Hallem S, Engler D. An empirical study of operating systems errors. In: Proc. of the ACM Symp. on Operating Systems Principles (SOSP 2001). New York: ACM Press, 2001. 73-88.[doi: 10.1145/502059.502042]
    [4] Swift MM, Martin S, Levy HM, Eggers SJ. Nooks: An architecture for reliable device drivers. In: Proc. of the ACM SIGOPS European Workshop. New York: ACM Press, 2002. 102-107.[doi: 10.1145/1133373.1133393]
    [5] Swift MM, Bershad BN, Levy HM. Improving the reliability of commodity operating systems. In: Proc. of the ACM Symp. on Operating Systems Principles. New York: ACM Press, 2003. 207-222.[doi: 10.1145/1165389.945466]
    [6] Swift MM, Annamalai M, Bershad BN, Levy HM. Recovering device drivers. ACM Trans. on Computer Systems, 2006,24(4):333-　360.[doi: 10.1145/1189256.1189257]
    [7] Herder JN, Bos H, Gras B, Homburg P, Tanenbaum AS. Failure resilience for device drivers. In: Proc. of the IEEE/IFIP Int'l Conf. on Dependable Systems and Networks (DSN). IEEE Press, 2007. 41-50.[doi: 10.1109/DSN.2007.46]
    [8] Hunt G, Larus J, Abadi M, Aiken M, Barham P, Fähndrich M, Hawblitzel C, Hodson O, Levi S, Murphy N, Steensgaard B, Tarditi D, Wobber D, Zill B. An overview of the singularity project. Technical Report, MSR-TR-2005-135, Washington: Microsoft Research, 2005.
    [9] Schulte W. From dependable multi-user to dependable multi-application operating systems: Invited talk. In: Proc. of the ACM Workshop on Secure Execution of Untrusted Code. New York: ACM Press, 2009. 1-2.[doi: 10.1145/1655077.1655079]
    [10] Hunt G, Aiken M, Fähndrich M, Mann T. Sealing OS processes to improve dependability and safety. In: Proc. of the ACM SIGOPS/EuroSys European Conf. on Computer Systems. New York: ACM Press, 2007. 341-354.[doi: 10.1145/1272998.1273032]
    [11] Hunt GC, Larus JR. Singularity: Rethinking the software stack. ACM SIGOPS Operating Systems Review, 2007,41(2):37-49.[doi: 10.1145/1243418.1243424]
    [12] Spear MF, Roeder T, Hodson O, Hunt GC, Levi S. Solving the starting problem: Device drivers as self-describing artifacts. In: Proc. of the ACM SIGOPS/EuroSys European Conf. on Computer Systems. New York: ACM Press, 2006. 45-57.[doi: 10.1145/1217935. 1217941]
    [13] David FM, Chan E, Carlyle JC, Campbell RH. CuriOS: Improving reliability through operating system structure. In: Proc. of the USENIX Conf. on Operating Systems Design and Implementation. USENIX Association, 2008. 59-72.
    [14] Rashid RF, Tokuda H. Mach: A system software kernel. Computing Systems in Engineering, 1990,1(2):163-169.
    [15] Forin A, Golub D, Bershad BN. An I/O system for Mach. In: Proc. of the USENIX Mach Symp. USENIX Association, 1991. 163–176.
    [16] Chiueh T, Venkitachalam G, Pradhan P. Integrating segmentation and paging protection for safe, efficient and transparent software extensions. In: Proc. of the ACM Symp. on Operating Systems Principles. New York: ACM Press, 1999. 140-153.[doi: 10.1145/ 346152.346187]
    [17] Oliveira D, Wetzel N, Bucci M, Navarro J, Sullivan D, Jin Y. Hardware-Software collaboration for secure coexistence with kernel extensions. ACM SIGAPP Applied Computing Review, 2014,14(3):22-35.[doi: 10.1145/2670967.2670969]
    [18] Oliveira D, Navarro J, Wetzel N, Bucci M. Ianus: Secure and holistic coexistence with kernel extensions3/4A immune system-inspired approach. In: Proc. of the 29th ACM Symp. on Applied Computing. New York: ACM Press, 2014. 1672-1679.[doi: 10. 1145/2554850.2554923]
    [19] Zhou Y, Wang X, Chen Y, Wang Z. ARMlock: Hardware-Based fault isolation for ARM. In: Proc. of the 2014 ACM SIGSAC Conf. on Computer and Communications Security. New York: ACM Press, 2014. 558-569.[doi: 10.1145/2660267.2660344]
    [20] Boyd-Wickizer S, Zeldovich N. Tolerating malicious device drivers in Linux. In: Proc. of the 2010 USENIX Annual Technical Conf. USENIX Association, 2010.
    [21] Leslie B, Chubb P, Fitzroy-Dale N, Götz S, Gray C, Macpherson L, Potts D, Shen YT, Elphinstone K, Heiser G. User-Level device drivers: Achieved performance. Journal of Computer Science and Technology, 2005,20(5):654-664.[doi: 10.1007/s11390-005-0654-4]
    [22] User-Mode driver framework. 2004. http://en.wikipedia.org/wiki/User-Mode_Driver_Framework
    [23] Microsoft Corporation. Architecture of the user-mode driver framework. Version 0.7. 2006. http://www.microsoft.com/whdc/ driver/wdf/UMDF-arch.mspx
    [24] Windows driver foundation. 2005. http://en.wikipedia.org/wiki/Windows_Driver_Foundation
    [25] MINIX 3. 1987. http://www.minix3.org/
    [26] Ganapathy V, Balakrishnan A, Swift MM, Jha S. Microdrivers: A new architecture for device drivers. In: Proc. of the 11th Workshop on Hot Topics in Operating Systems (HotOS XI). 2007.
    [27] Ganapathy V, Renzelmann MJ, Balakrishnan A, Swift MM, Jha S. The design and implementation of microdrivers. In: Proc. of the Int'l Conf. on Architectural Support for Programming Languages and Operating Systems. New York: ACM Press, 2008. 168-178.[doi: 10.1145/1346281.1346303]
    [28] Fraser K, Hand S, Neugebauer R, Pratt I, Warfield A, Williamson M. Safe hardware access with the Xen virtual machine monitor. In: Proc. of the Workshop on Operating System and Architectural Support for the on demand IT InfraStructure (OASIS). 2004.
    [29] Barham P, Dragovic B, Fraser K, Hand S, Harris T, Ho A, Neugebauer R, Pratt I, Warfield A. Xen and the art of virtualization. In: Proc. of the ACM Symp. on Operating Systems Principles. New York: ACM Press, 2003. 164-177.[doi: 10.1145/945445.945462]
    [30] Pratt I, Fraser K, Hand S, Limpach C, Warfield A. Xen 3.0 and the art of virtualization. In: Proc. of the Linux Symp. 2005. 65.
    [31] Matthews JN, Dow EM, Deshane T, Hu W, Bongio J, Wilbur PF, Johnson B. Running Xen: A Hands-on Guide to the Art of Virtualization. Prentice Hall PTR, 2008.
    [32] Erlingsson U, Roeder T, Wobber T. Virtual environments for unreliable extensions. Microsoft Research Techical Report, MSR-TR-2005-82, Microsoft Corporation, 2005.
    [33] LeVasseur J, Uhlig V, Stoess J, Götz S. Unmodified device driver reuse and improved system dependability via virtual machines. In: Proc. of the Symp. on Operating Systems Design and Implementation. USENIX Association, 2004. 17-30.
    [34] Wahbe R, Lucco S, Anderson TE, Graham SL. Efficient software-based fault isolation. In: Proc. of the ACM Symp. on Operating Systems Principles. New York: ACM Press, 1994. 203-216.[doi: 10.1145/173668.168635]
    [35] Zhou F, Condit J, Anderson Z, Bagrak I, Ennals R, Harren M, Necula G, Brewer E. SafeDrive: Safe and recoverable extensions using language-based techniques. In: Proc. of the Symp. on Operating Systems Design and Implementation. USENIX Association, 2006. 45-60.
    [36] Herder JN, Bos H, Gras B, Homburg P, Tanenbaum AS. Fault isolation for device drivers. In: Proc. of the IEEE/IFIP Int'l Conf. on Dependable Systems and Networks (DSN). IEEE Press, 2009. 33-42.[doi: 10.1109/DSN.2009.5270357]
    [37] Ryzhyk L, Zhu Y, Heiser G. The case for active device drivers. In: Proc. of the Asia-Pacific Workshop on Systems. New York: ACM Press, 2010. 25-30.[doi: 10.1145/1851276.1851283]
    [38] Kadav A, Renzelmann MJ, Swift MM. Fine-Grained fault tolerance using device checkpoints. In: Proc. of the Int'l Conf. on Architectural Support for Programming Languages and Operating Systems. New York: ACM Press, 2013. 473-484.[doi: 10.1145/ 2451116.2451168]
    [39] Ball T, Bounimova E, Cook B, Levin V, Lichtenberg J, McGarvey CM, Ondrusek B, Rajamani SK, Ustuner A. Thorough static analysis of device drivers. In: Proc. of the ACM SIGOPS/EuroSys European Conf. on Computer Systems. New York: ACM Press, 2006. 73-85.[doi: 10.1145/1218063.1217943]
    [40] Henzinger TA, Jhala R, Majumdar R, Sutre G. Software verification with BLAST. In: Model Checking Software. Berlin, Heidelberg: Springer-Verlag, 2003. 235-239.[doi: 10.1007/3-540-44829-2_17]
    [41] Beyer D, Chlipala AJ, Henzinger TA, Jhala R, Majumdar R. The Blast query language for software verification. In: Static Analysis. Berlin, Heidelberg: Springer-Verlag, 2004. 2-18.[doi: 10.1007/978-3-540-27864-1_2]
    [42] Beyer D, Henzinger TA, Jhala R, Majumdar R. The software model checker Blast. Int'l Journal on Software Tools for Technology Transfer, 2007,9(5-6):505-525.[doi: 10.1007/s10009-007-0044-z]
    [43] Ryzhyk L, Kuz I, Heiser G. Formalising device driver interfaces. In: Proc. of the Workshop on Programming Languages and Operating Systems. New York: ACM Press, 2007.[doi: 10.1145/1376789.1376803]
    [44] Amani S, Ryzhyk L, Donaldson AF, Heiser Gernot, Legg A, Zhu Y. Static analysis of device drivers: We can do better! In: Proc. of the Asia-Pacific Workshop on Systems. New York: ACM Press, 2011.[doi: 10.1145/2103799.2103809]
    [45] Engler D, Chelf B, Chou A, Hallem S. Checking system rules using system-specific, programmer-written compiler extensions. In: Proc. of the Conf. on Symp. on Operating System Design & Implementation, Vol.4. USENIX Association, 2000. 1-1.
    [46] Ashcraft K, Engler D. Using programmer-written compiler extensions to catch security holes. In: Proc. of the IEEE Symp. on Security and Privacy. IEEE Press, 2002. 143-159.[doi: 10.1109/SECPRI.2002.1004368]
    [47] Ball T, Bounimova E, Kumar R, Levin V. SLAM2: Static driver verification with under 4% false alarms. In: Proc. of the Conf. on Formal Methods in Computer-Aided Design. FMCAD Inc., 2010. 35-42.
    [48] Ryzhyk L, Chubb P, Kuz I, Heiser G. Dingo: Taming device drivers. In: Proc. of the 4th ACM European Conf. on Computer Systems. New York: ACM Press, 2009. 275-288.[doi: 10.1145/1519065.1519095]
    [49] Kinder J, Veith H. Precise static analysis of untrusted driver binaries. In: Proc. of the Conf. on Formal Methods in Computer-Aided Design. FMCAD Inc., 2010. 43-50.
    [50] Williams D, Reynolds P, Walsh K, Sirer EG, Schneider FB. Device driver safety through a reference validation mechanism. In: Proc. of the USENIX Conf. on Operating Systems Design and Implementation. USENIX Association, 2008. 241-254.
    [51] Kadav A, Renzelmann MJ, Swift MM. Tolerating hardware device failures in software. In: Proc. of the ACM Symp. on Operating Systems Principles. New York: ACM Press, 2009. 59-72.[doi: 10.1145/1629575.1629582]
    [52] Condit J, Harren M, McPeak S, Necula GC, Weimer W. CCured in the real world. ACM SIGPLAN Notices, 2003,38(5):232-244.[doi: 10.1145/780822.781157]
    [53] Erlingsson U, Abadi M, Vrable M, Budiu M, Necula GC. XFI: Software guards for system address spaces. In: Proc. of the Symp. on Operating Systems Design and Implementation. USENIX Association, 2006. 75-88.
    [54] Mao Y, Chen H, Zhou D, Wang X, Zeldovich N, Kaashoek MF. Software fault isolation with API integrity and multi-principal modules. In: Proc. of the ACM Symp. on Operating Systems Principles. New York: ACM Press, 2011. 115-128.[doi: 10.1145/ 2043556.2043568]
    [55] Microsoft and 3Com Corporation. Network Driver Interface Specification. 1989. http://www.ndis.com/
    [56] Apple and Novell Corporation. Open data-link interface. 1992. http://support.novell.com/techcenter/articles/ana19921103.html
    [57] Uniform driver interface. 1999. http://www.projectudi.org/
    [58] Mérillon F, Réveillère L, Consel C, Marlet R, Muller G. Devil: An IDL for hardware programming. In: Proc. of the Conf. on Symp. on Operating System Design & Implementation, Vol.4. USENIX Association, 2000. 2-2.
    [59] Réveillère L, Muller G. Improving driver robustness: An evaluation of the Devil approach. In: Proc. of the IEEE/IFIP Int'l Conf. on Dependable Systems and Networks (DSN). IEEE Press, 2001. 131-140.[doi: 10.1109/DSN.2001.941399]
    [60] Conway CL, Edwards SA. NDL: A domain-specific language for device drivers. ACM Sigplan Notices, 2004,39(7):30-36.[doi: 10. 1145/998300.997169]
    [61] Sun J, Yuan W, Kallahalla M, Islam N. HAIL: A language for easy and correct device access. In: Proc. of the 5th ACM Int'l Conf. on Embedded Software. New York: ACM Press, 2005. 1-9.[doi: 10.1145/1086228.1086230]
    [62] Wittie L. Laddie: The language for automated device drivers (ver 1). Technical Report, 08-2, Bucknell CS-TR, 2008.
    [63] Schüpbach A, Baumann A, Roscoe T, Peter S. A declarative language approach to device configuration. ACM Trans. on Computer Systems, 2012,30(1):5.[doi: 10.1145/1950365.1950382]
    [64] Wang S, Malik S, Bergamaschi RA. Modeling and integration of peripheral devices in embedded systems. In: Proc. of the Conf. on Design, Automation and Test in Europe, Vol.1. IEEE Press, 2003. 136-141.[doi: 10.1109/DATE.2003.1253599]
    [65] Ryzhyk L, Chubb P, Kuz I, Sueur EL, Heiser G. Automatic device driver synthesis with termite. In: Proc. of the ACM Symp. on Operating Systems Principles. New York: ACM Press, 2009. 73-86.[doi: 10.1145/1629575.1629583]
    [66] Ryzhyk L, Walker A, Keys J, Legg A, Raghunath A, Stumm M, Vij M. User-Guided device driver synthesis. In: Proc. of the USENIX Conf. on Operating Systems Design and Implementation. USENIX Association, 2014. 661-676.
    [67] O'Nils M, Jantsch A. Device driver and DMA controller synthesis from HW/SW communication protocol specifications. Design Automation for Embedded Systems, 2001,6(2):177-205.[doi: 10.1023/A:1011246731756]
    [68] Hsieh WC, Fiuczynski ME, Garrett C, Savage S, Becker D, Bershad BN. Language support for extensible operating systems. In: Proc. of the Workshop on Compiler Support for System Software. 1996. 127.
    [69] Von Eicken T, Chang CC, Czajkowski G, Hawblitzel C, Hu D, Spoonhower D. J-Kernel: A capability-based operating system for Java. In: Proc. of the Secure Internet Programming. Berlin, Heidelberg: Springer-Verlag, 1999. 369-393.[doi: 10.1007/3-540-48749-2_17]
    [70] Yamauchi H, Wolczko M. Writing Solaris device drivers in Java. In: Proc. of the 3rd Workshop on Programming Languages and Operating Systems: Linguistic Support for Modern Operating Systems. New York: ACM Press, 2006.[doi: 10.1145/1215995. 1215998]
    [71] Okumura T, Childers BR, Mosse D. Running a Java VM inside an operating system kernel. In: Proc. of the 4th ACM SIGPLAN/ SIGOPS Int'l Conf. on Virtual Execution Environments. New York: ACM Press, 2008. 161-170.[doi: 10.1145/1346256.1346279]
    [72] Renzelmann MJ, Swift MM. Decaf: Moving device drivers to a modern language. In: Proc. of the USENIX Annual Technical Conf. USENIX Association, 2009.
    [73] Chandrasekaran P, Conway CL, Joy JM, Rajamani SK. Programming asynchronous layers with CLARITY. In: Proc. of the 6th Joint Meeting of the European Software Engineering Conf. and the ACM SIGSOFT Symp. on the Foundations of Software Engineering. New York: ACM Press, 2007. 65-74.[doi: 10.1145/1287624.1287636]
    [74] Chen H, Godet-Bar G, Rousseau F, Petrot F. Me3D: A model-driven methodology expediting embedded device driver development. In: Proc. of the 22nd IEEE Int'l Symp. on Rapid System Prototyping (RSP). IEEE Press, 2011. 171-177.[doi: 10.1109/RSP.2011. 5929992]
    相似文献
    引证文献
引用本文

张一帆,黄超,欧建生,汤恩义,陈鑫.设备驱动程序可靠性和正确性保障方法与技术研究进展.软件学报,2015,26(2):239-253

复制
相关视频

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

京公网安备 11040202500063号