Towards static flow-based declassification for legacy and untrusted programs

Bruno P.S. Rocha, Sruthi Bandhakavi, Jeremy den Hartog, William H. Winsborough, Sandro Etalle

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    11 Citations (Scopus)
    128 Downloads (Pure)


    Simple non-interference is too restrictive for specifying and enforcing information flow policies in most programs. Exceptions to non-interference are provided using declassification policies. Several approaches for enforcing declassification have been proposed in the literature. In most of these approaches, the declassification policies are embedded in the program itself or heavily tied to the variables in the program being analyzed, thereby providing little separation between the code and the policy. Consequently, the previous approaches essentially require that the code be trusted, since to trust that the correct policy is being enforced, we need to trust the source code. In this paper, we propose a novel framework in which declassification policies are related to the source code being analyzed via its I/O channels. The framework supports many of the of declassification policies identified in the literature. Based on flow-based static analysis, it represents a first step towards a new approach that can be applied to untrusted and legacy source code to automatically verify that the analyzed program complies with the specified declassification policies. The analysis works by constructing a conservative approximation of expressions over input channel values that could be output by the program, and by determining whether all such expressions satisfy the declassification requirements stated in the policy. We introduce a representation of such expressions that resembles tree automata. We prove that if a program is considered safe according to our analysis then it satisfies a property we call Policy Controlled Release, which formalizes information-flow correctness according to our notion of declassification policy. We demonstrate, through examples, that our approach works for several interesting and useful declassification policies, including one involving declassification of the average of several confidential values.
    Original languageUndefined
    Title of host publicationIEEE Symposium on Security and Privacy
    Place of PublicationUSA
    PublisherIEEE Society Press
    Number of pages16
    ISBN (Print)978-0-7695-4035-1
    Publication statusPublished - 16 May 2010
    Event31st IEEE Symposium on Security and Privacy 2010 - The Claremont Resort, Oakland, United States
    Duration: 16 May 201019 May 2010
    Conference number: 31

    Publication series

    PublisherIEEE Society Press
    ISSN (Print)1081-6011


    Conference31st IEEE Symposium on Security and Privacy 2010
    Country/TerritoryUnited States
    Internet address


    • METIS-276218
    • EWI-19077
    • SCS-Cybersecurity
    • IR-75226

    Cite this