Static Analysis of Processes for No Read-Up and No Write-Down

C. Bodei, P. Degano, Flemming Nielson, Hanne Riis Nielson

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


    We study a variant of the no read-up/no write-down security property of Bell and LaPadula for processes in the π-calculus. Once processes are given levels of security clearance, we statically check that a process at a high level never sends names to processes at a lower level. The static check is based on a Control Flow Analysis for the π-calculus that establishes a super-set of the set of names to which a given name may be bound and of the set of names that may be sent and received along a given channel, taking into account its directionality. The static check is shown to imply the natural dynamic condition.
    Original languageEnglish
    Title of host publicationProc. FOSSACS'99
    PublisherSpringer Verlag
    Publication date1999
    Publication statusPublished - 1999
    EventProc. FOSSACS'99 -
    Duration: 1 Jan 1999 → …


    ConferenceProc. FOSSACS'99
    Period01/01/1999 → …

    Fingerprint Dive into the research topics of 'Static Analysis of Processes for No Read-Up and No Write-Down'. Together they form a unique fingerprint.

    Cite this