Citation
Rabe Markus. "A Temporal Logic Approach to Information-Flow Control". Talk or presentation, 22, September, 2015.

Abstract
Information-flow control is a principled approach to prevent vulnerabilities in programs and other technical systems. In information-flow control we define information-flow properties, which are sufficient conditions for when the system is secure in a particular attack scenario, and then enforce that the given system adheres to its properties. Information-flow properties refer to how the information flows through the system and standard verification approaches seemed to be inapplicable. In this talk I present recent work on a temporal logic approach to information-flow control. We discuss how temporal logics can be used to provide a simple formal basis for the specification and enforcement (in our case model checking) of information-flow properties. The main challenge of this approach is that the standard temporal logics are unable to express these properties. They lack the ability to relate multiple executions of a system, which is the essential feature of information-flow properties. We thus extend temporal logics by the ability to quantify over multiple executions and to relate them using boolean and temporal operators. We show that the approach supports a wide range of previously known and also new information-flow properties with a single model checking algorithm. We demonstrate the effectiveness of the approach along case studies in hardware security.

Electronic downloads

• seminar.2015-09-22.Markus_Rabe.pdf · application/pdf · 1134 kbytes

• HTML

  Rabe Markus. <a
  href="http://chess.eecs.berkeley.edu/pubs/1116.html"
  ><i>A Temporal Logic Approach to Information-Flow
  Control</i></a>, Talk or presentation,  22,
  September, 2015.

• Plain text

  Rabe Markus. "A Temporal Logic Approach to
  Information-Flow Control". Talk or presentation,  22,
  September, 2015.

• BibTeX

  @presentation{Markus15_TemporalLogicApproachToInformationFlowControl,
      author = {Rabe Markus},
      title = {A Temporal Logic Approach to Information-Flow
                Control},
      day = {22},
      month = {September},
      year = {2015},
      abstract = {Information-flow control is a principled approach
                to prevent vulnerabilities in programs and other
                technical systems. In information-flow control we
                define information-flow properties, which are
                sufficient conditions for when the system is
                secure in a particular attack scenario, and then
                enforce that the given system adheres to its
                properties. Information-flow properties refer to
                how the information flows through the system and
                standard verification approaches seemed to be
                inapplicable. In this talk I present recent work
                on a temporal logic approach to information-flow
                control. We discuss how temporal logics can be
                used to provide a simple formal basis for the
                specification and enforcement (in our case model
                checking) of information-flow properties. The main
                challenge of this approach is that the standard
                temporal logics are unable to express these
                properties. They lack the ability to relate
                multiple executions of a system, which is the
                essential feature of information-flow properties.
                We thus extend temporal logics by the ability to
                quantify over multiple executions and to relate
                them using boolean and temporal operators. We show
                that the approach supports a wide range of
                previously known and also new information-flow
                properties with a single model checking algorithm.
                We demonstrate the effectiveness of the approach
                along case studies in hardware security. },
      URL = {http://chess.eecs.berkeley.edu/pubs/1116.html}
  }
  

Posted by Sadigh Dorsa on 23 Sep 2015.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.