5

Inferring data polymorphism in systems code

 3 years ago
source link: https://dl.acm.org/doi/10.1145/2025113.2025159
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
neoserver,ios ssh client

ABSTRACT

We describe techniques for analyzing data polymorphism in C, and show that understanding data polymorphism is important for statically verifying type casts in the Linux kernel, where our techniques prove the safety of 75% of downcasts to structure types, out of a population of 28767. We also discuss prevalent patterns of data polymorphism in Linux, including code patterns we can handle and those we cannot.

References

  1. Cyclone: User Manual. http://cyclone.thelanguage.org/wiki/User Manual.
  2. Deputy Manual. http://deputy.cs.berkeley.edu/manual.html.
  3. Alex Aiken, Suhabe Bugrara, Iisil Dillig, Thomas Dillig, Peter Hawkins, and Brian Hackett. An overview of the saturn project. In Workshop on Program Analysis for Software Tools and Engineering, 2007.
  4. Suhabe Bugrara and Alex Aiken. Verifying the safety of user pointer dereferences. In IEEE Symposium on Security and Privacy, pages 325--338, 2008.
  5. Jeremy Condit, Brian Hackett, Shuvendu Lahiri, and Shaz Qadeer. Unifying type checking and property checking for low-level code. In Principles of Programming Languages, 2009.
  6. Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George Necula. Dependent types for low-level programming. In European Symposium on Programming, 2007.
  7. Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, and Westley Weimer. CCured in the real world. In Programming Language Design and Implementation, 2003.
  8. Manuvir Das, Sorin Lerner, and Mark Seigle. Program verification in polynomial time. In Conference on Programming Language Design and Implementation, pages 57--68, 2002.
  9. Dan Grossman. Quantified types in an imperative language. ACM Transactions on Programming Languages and Systems, 28, 2006.
  10. Dan Grossman, Michael Hicks, Trevor Jim, and Greg Morrisett. Cyclone: a type-safe dialect of C. In C/C++ Users Journal, volume 23, 2005.
  11. Brian Hackett. Type Safety in the Linux Kernel. PhD thesis, Stanford University, 2010.
  12. Brian Hackett and Alex Aiken. How is aliasing used in systems software? In Foundations of Software Engineering, 2006.
  13. Seth Hallen, Benjamin Chelf, Yichen Xie, and Dawson Engler. A system and language for building system-specific, static analyses. In Conference on Programming Language Design and Implementation, pages 69--82, 2002.
  14. Robert Johnson and David Wagner. Finding user/kernel pointer bugs with type inference. In USENIX Security Symposium, pages 119--134, 2004.
  15. Shuvendu Lahiri and Shaz Qadeer. Back to the future: Revisiting precise program verification using SMT solvers. In Principles of Programming Languages, 2008.
  16. Alexey Loginov, Suan Hsi Yong, Susan Horwitz, and Thomas Reps. Debugging via run-time type checking. In In Proceedings of FASE 2001: Fundamental Approaches to Software Engineering, pages 217--232. Springer, 2001.
  17. George C. Necula, Scott McPeak, and Westley Weimer. CCured: Type-safe retrofitting of legacy software. In Principles of Programming Languages, 2002.
  18. Michael Siff, Satish Chandra, Thomas Ball, Krishna Kunchithapadam, and Thomas Reps. Coping with type casts in C. In Foundations of Software Engineering, 1999.
  19. Yichen Xie and Alex Aiken. Scalable error detection using boolean satisfiability. In Principles of Programming Languages, 2005.

Comments

0 Comments


report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK