UMD Theses and Dissertations
Permanent URI for this collectionhttp://hdl.handle.net/1903/3
New submissions to the thesis/dissertation collections are added automatically as they are received from the Graduate School. Currently, the Graduate School deposits all theses and dissertations from a given semester after the official graduation date. This means that there may be up to a 4 month delay in the appearance of a given thesis/dissertation in DRUM.
More information is available at Theses and Dissertations at University of Maryland Libraries.
Browse
2 results
Search Results
Item Mechanizing Abstract Interpretation(2017) Darais, David Charles; Van Horn, David; Computer Science; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)It is important when developing software to verify the absence of undesirable behavior such as crashes, bugs and security vulnerabilities. Some settings require high assurance in verification results, e.g., for embedded software in automobiles or airplanes. To achieve high assurance in these verification results, formal methods are used to automatically construct or check proofs of their correctness. However, achieving high assurance for program analysis results is challenging, and current methods are ill suited for both complex critical domains and mainstream use. To verify the correctness of software we consider program analyzers---automated tools which detect software defects---and to achieve high assurance in verification results we consider mechanized verification---a rigorous process for establishing the correctness of program analyzers via computer-checked proofs. The key challenges to designing verified program analyzers are: (1) achieving an analyzer design for a given programming language and correctness property; (2) achieving an implementation for the design; and (3) achieving a mechanized verification that the implementation is correct w.r.t. the design. The state of the art in (1) and (2) is to use abstract interpretation: a guiding mathematical framework for systematically constructing analyzers directly from programming language semantics. However, achieving (3) in the presence of abstract interpretation has remained an open problem since the late 1990's. Furthermore, even the state-of-the art which achieves (3) in the absence of abstract interpretation suffers from the inability to be reused in the presence of new analyzer designs or programming language features. First, we solve the open problem which has prevented the combination of abstract interpretation (and in particular, calculational abstract interpretation) with mechanized verification, which advances the state of the art in designing, implementing, and verifying analyzers for critical software. We do this through a new mathematical framework Constructive Galois Connections which supports synthesizing specifications for program analyzers, calculating implementations from these induced specifications, and is amenable to mechanized verification. Finally, we introduce reusable components for implementing analyzers for a wide range of designs and semantics. We do this though two new frameworks Galois Transformers and Definitional Abstract Interpreters. These frameworks tightly couple analyzer design decisions, implementation fragments, and verification properties into compositional components which are (target) programming-language independent and amenable to mechanized verification. Variations in the analysis design are then recovered by simply re-assembling the combination of components. Using this framework, sophisticated program analyzers can be assembled by non-experts, and the result are guaranteed to be verified by construction.Item Modeling, Quantifying, and Limiting Adversary Knowledge(2015) Mardziel, Piotr; Hicks, Michael; Computer Science; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)Users participating in online services are required to relinquish control over potentially sensitive personal information, exposing them to intentional or unintentional miss-use of said information by the service providers. Users wishing to avoid this must either abstain from often extremely useful services, or provide false information which is usually contrary to the terms of service they must abide by. An attractive middle-ground alternative is to maintain control in the hands of the users and provide a mechanism with which information that is necessary for useful services can be queried. Users need not trust any external party in the management of their information but are now faced with the problem of judging when queries by service providers should be answered or when they should be refused due to revealing too much sensitive information. Judging query safety is difficult. Two queries may be benign in isolation but might reveal more than a user is comfortable with in combination. Additionally malicious adversaries who wish to learn more than allowed might query in a manner that attempts to hide the flows of sensitive information. Finally, users cannot rely on human inspection of queries due to its volume and the general lack of expertise. This thesis tackles the automation of query judgment, giving the self-reliant user a means with which to discern benign queries from dangerous or exploitive ones. The approach is based on explicit modeling and tracking of the knowledge of adversaries as they learn about a user through the queries they are allowed to observe. The approach quantifies the absolute risk a user is exposed, taking into account all the information that has been revealed already when determining to answer a query. Proposed techniques for approximate but sound probabilistic inference are used to tackle the tractability of the approach, letting the user tradeoff utility (in terms of the queries judged safe) and efficiency (in terms of the expense of knowledge tracking), while maintaining the guarantee that risk to the user is never underestimated. We apply the approach to settings where user data changes over time and settings where multiple users wish to pool their data to perform useful collaborative computations without revealing too much information. By addressing one of the major obstacles preventing the viability of personal information control, this work brings the attractive proposition closer to reality.