Show simple item record

dc.contributor.authorGunawi, Haryadi S.en_US
dc.contributor.authorKrishnan, Shwetaen_US
dc.description.abstractThe storage stack is not trustworthy due to errors that arise from a variety of sources: unreliable hardware, malicious errors and file system bugs. Today, software errors play a dominant role due to their inherent complexity. In the first part of our project, we look towards verifying a specific file system property: on-disk pointer manipulation. We utilize CQUAL, a framework for adding type qualifiers with type inference support, and apply our analysis to the Linux ext2 file system. We find that adding qualifiers serves the valuable purpose of ensuring that on-disk pointers are accessed and manipulated correctly by the file system. Thus, we believe that the qualifiers we introduce would decrease the probability of bugs being introduced by file system programmers. We also describe our experience in using CQUAL and discuss its limitations. Based on our experience with CQUAL, we come up with a second analysis, a buffer management verifier, that fits better with the power of CQUAL by being simpler, yet more widely applicable to different file systems than the first analysis.en_US
dc.publisherUniversity of Wisconsin-Madison Department of Computer Sciencesen_US
dc.titleVerifying File System Properties with Type Inferenceen_US
dc.typeTechnical Reporten_US

Files in this item


This item appears in the following Collection(s)

  • CS Technical Reports
    Technical Reports Archive for the Department of Computer Sciences at the University of Wisconsin-Madison

Show simple item record