"Winning Cybersecurity Paper Addresses Algorithm Accuracy"

The 10th Annual Best Scientific Cybersecurity Paper Competition honors the best foundational cybersecurity paper published in 2021. The winning paper titled "Verifying Hyperproperties with Temporal Logic of Actions (TLA)," written by Leslie Lamport and Fred B. Schneider, from Microsoft Research and Cornell University, respectively, delves into ensuring the correctness of a computer algorithm. According to the paper, most security tools examine specific parts of code rather than the algorithm itself. Lamport and Schneider recommend looking at the theoretical and practical breakthroughs to verify algorithm and, potentially, system accuracy. The researchers demonstrate how to verify that an algorithm meets the necessary hyperproperties to capture correctness. Hyperproperties are sets of properties that can describe security policies, such as secure information flow, which properties alone cannot. These must be understood in terms of several runs of a program, such as if the value of one variable predicts something pertaining to the value of another (i.e., whether information is leaking). The winning work reflects the transformative insight that these hyperproperties may be formulated using the TLA, which is a means to describe systems in a single mathematic formula. This coupling to an existing toolset allows the study of hyperproperties in future cybersecurity research and development. This article continues to discuss the 10th Annual Best Scientific Cybersecurity Paper Competition, the winning cybersecurity paper that addresses algorithm accuracy, and other work honored by the competition.  

NSA reports "Winning Cybersecurity Paper Addresses Algorithm Accuracy"