Date Posted: 7/15/2021

Fred B. Schneider, Samuel B. Eckert Professor of Computer Science in the Ann S. Bowers College of Computing and Information Science, has received a Distinguished Paper Award at the 34th IEEE Computer Security Foundations (CSF) Symposium for his "Verifying Hyperproperties with TLA," which he coauthored with Microsoft Research Distinguished Scientist, Leslie Lamport.

About the significance of his award-winning research, Schneider remarks: "Whereas previously people have been developing new logics for proving that a system satisfies a hyperproperty, this work showed that an old logic will work just fine. Moreover, the logic we used (TLA) is already known and used by practitioners in industry and there already exist model checkers, proof checkers, and other tools. Back to the future?" And about the organization that granted the award, Schneider notes that "CSF itself is an annual symposium that brings together people who are interested in a science base for cyber-security."

Abstract of "Verifying Hyperproperties with TLA": Hyperproperties generalize ordinary properties by expressing relations among multiple executions of a system. Self composition has been used to reduce verifying that a system satisfies certain classes of hyperproperties to verifying that a derived system satisfies an ordinary property. By describing systems and their properties in the temporal logic TLA, we use self-composition to handle a larger class of hyperproperties that includes those we have seen that express security conditions. TLA tools are used to verify that high-level designs of industrial systems satisfy properties. Now, they can also verify that those systems satisfy these hyperproperties. No prior knowledge of hyperproperties or TLA is assumed.