• Login
    JavaScript is disabled for your browser. Some features of this site may not work without it.
    Model Counting Modulo Theories 
    •   QMRO Home
    • Queen Mary University of London Theses
    • Theses
    • Model Counting Modulo Theories
    •   QMRO Home
    • Queen Mary University of London Theses
    • Theses
    • Model Counting Modulo Theories
    ‌
    ‌

    Browse

    All of QMROCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects
    ‌
    ‌

    Administrators only

    Login
    ‌
    ‌

    Statistics

    Most Popular ItemsStatistics by CountryMost Popular Authors

    Model Counting Modulo Theories

    View/Open
    Phan_Quoc-Sang_PhD_Final_150915.pdf (1012.Kb)
    Publisher
    Queen Mary University of London
    Metadata
    Show full item record
    Abstract
    This thesis is concerned with the quantitative assessment of security in software. More specifically, it tackles the problem of efficient computation of channel capacity, the maximum amount of confidential information leaked by software, measured in Shannon entropy or R²nyi's min-entropy. Most approaches to computing channel capacity are either efficient and return only (possibly very loose) upper bounds, or alternatively are inefficient but precise; few target realistic programs. In this thesis, we present a novel approach to the problem by reducing it to a model counting problem on first-order logic, which we name Model Counting Modulo Theories or #SMT for brevity. For quantitative security, our contribution is twofold. First, on the theoretical side we establish the connections between measuring confidentiality leaks and fundamental verification algorithms like Symbolic Execution, SMT solvers and DPLL. Second, exploiting these connections, we develop novel #SMT-based techniques to compute channel capacity, which achieve both accuracy and efficiency. These techniques are scalable to real-world programs, and illustrative case studies include C programs from Linux kernel, a Java program from a European project and anonymity protocols. For formal verification, our contribution is also twofold. First, we introduce and study a new research problem, namely #SMT, which has other potential applications beyond computing channel capacity, such as returning multiple-counterexamples for Bounded Model Checking or automated test generation. Second, we propose an alternative approach for Bounded Model Checking using classical Symbolic Execution, which can be parallelised to leverage modern multi-core and distributed architecture. For software engineering, our first contribution is to demonstrate the correspondence between the algorithm of Symbolic Execution and the DPLL(T ) algorithm used in state-of-the-art SMT solvers. This correspondence could be leveraged to improve Symbolic Execution for automated test generation. Finally, we show the relation between computing channel capacity and reliability analysis in software.
    Authors
    Phan, Quoc-Sang
    URI
    http://qmro.qmul.ac.uk/xmlui/handle/123456789/15130
    Collections
    • Theses [3321]
    Copyright statements
    The copyright of this thesis rests with the author and no quotation from it or information derived from it may be published without the prior written consent of the author
    Twitter iconFollow QMUL on Twitter
    Twitter iconFollow QM Research
    Online on twitter
    Facebook iconLike us on Facebook
    • Site Map
    • Privacy and cookies
    • Disclaimer
    • Accessibility
    • Contacts
    • Intranet
    • Current students

    Modern Slavery Statement

    Queen Mary University of London
    Mile End Road
    London E1 4NS
    Tel: +44 (0)20 7882 5555

    © Queen Mary University of London.