CS 590-MPL: Advanced Topics in Programming Languages

TTh 1:30p-2:45 LWSN 1106

about

Instructor:

Ben Delaware

bendy at purdue.edu

Office Hours: By Appointment

COVID-19 Addendum

Course Description:

Over the last several decades, the programming languages and formal methods communities have made significant progress toward ensuring that a program is correct with respect to some specification of its intended behavior, e.g. that an implementation of quicksort always returns a sorted list, a gradebook application correctly calculates the average test score, or that a program is free of any divide by zero errors. These communities have developed a number of techniques to automatically verify these sorts of properties, to the point that these techniques have been adopted to verify a wide variety of real-world systems, from device drivers at Microsoft, to absence of null pointer exceptions and concurrency bugs in Android and Java applications at Facebook.

The vast majority of these techniques deal with specifications of the behavior of a single execution of a program. Many desirable program behaviors fall outside this class, however, and require specifications that can describe multiple program executions. Somewhat surprisingly, examples of such relational properties or hyperproperties include foundational programming language concepts like parametricity, program refinement, and compiler correctness. Hyperproperties also abound in other computer science communities, including security ( absence of information leakeage) multiparty computation) databases (weak consistency), and AI (fairness, robustness).

This seminar will consider both the specification of a wide variety of hyperproperties, as well as the verification of programs with respect to relational specifications. Importantly, this class will strive to appreciate hyperproperties from the perspective of the communities that created them, in order to better connect them to a more PL/FM-view. To this end, the last fourth of the class will be an in-depth look at secure multiparty computation and how PL techniques for relational reasoning can be applied in that setting.

policies

Format: (Now with COVID-19 Bits!)

COVID-19 Addendum:

Starting March 23rd, all classes at Purdue must be delivered by remote instruction until the end of the Spring 2020 semester due to the COVID-19 Pandemic. We will thus be transitioning to a more discussion-based seminar focused on readings of recent research papers. While we won't be able to fully replicate the liveliness of our previous in-class discussions, I'm optimistic we can create a reasonable facsimile.

We will be using Zoom to carry out our online discussions, taking any overflow or asynchronous discussion to the class Slack. The link to the Zoom meeting is available on the course Slack channel. The structure will mimic our previous format, with each paper being assigned a designated facilitator to lead the discussion. The complete paper schedule is listed on this course website, now that everyone has had a chance to voice their paper and scheduling preferences on Slack.

Original Format:

This seminar course will be a complementary mixture of lectures and discussion of paper readings. Lectures will provide an introduction to important concepts, while the paper discussions will provide an in-depth look at the application of those concepts. Each paper will have a designated facilitator responsible for leading the discussion. To ensure a lively discussion, students will be responsible reading assigned papers at sufficient level to summarize the the research problem, the proposed solution, the relationship to existing work, and the evaluation of any claimed contributions.

Professor Delaware's meme-game is slightly out of touch with the PL youths of today (alright-- sorely out of touch). In order to address this problem, he asks that facilitators prepare at least one hip and cool meme about their paper (the other students are welcome to submit memes as well). At the end of class, the professor will leverage his considerable clout to reward these efforts by:

  • tweeting a "best of" gallery of the choicest memes
  • a distringuished tweet crowning a Queen or King of PL memes

Given the weakness of Professor Delaware's meme game, the selection of choice memes and the crowning of their royal memeness will be carried out by a class voite.

Note to auditors: Glad to have you onboard! In order to fairly distribute the discussion workload, I ask that you lead one to two classes during the semester.

Students will develop (in concert with the instructor) and work on an open-ended project over course of the semester. Ideally this will be an application of relational reasoning to their personal interests. Students are welcome to pair up for more ambitious projects. The project will include a short final report and presentation during the last week of class.

Discussion Forum:

A slack channel for the course will serve as the discussion board; all course announcements will also be posted there.

Grading:

Final grades will be assigned according to the following breakdown:

Class Project 40%
Facilitating Discussion 30%
Participation 30%

learning objectives:

At the end of the course, participants should be able to:

  • Precisely define hyperproperty, and distinguish between k-safety and k-liveness hyperproperties.
  • Identify and define examples of existing relational program properties drawn from both classical and recent literature, including:
    • PL-centric hyperproperties:
      • Data Abstraction
      • Bisimularity
      • Refinement
      • Compiler Correctness
    • Security-centric hyperproperties:
      • Non-interference with Delimited Release
      • Secure Multiparty Computation (Secure Realizability)
      • Cryptographic security
    • AI-centric hyperproperties:
      • Robustness
      • "Explainable AI" (Facts and Foils)
      • Fairness
    • Database-centric properties:
      • ACID (Weak Consistency)
    • System Properties
      • Crash Safety
      • Correctness of Operating System
  • Apply proof techniques for reasoning about relational properties:
    • General Relational Reasoning
      • Relational Program Logics
      • Product Programs
    • PL-centric:
      • Logical Relations
      • Coinduction
      • Stepwise Refinement / Correct-by-Construction Design
    • Security-centric:
      • Information Flow Analysis
      • Universal Composition Theorems
    • AI-centric
      • Robustness
      • Fairness Papers
    • Database-centric:
      • TBD
    • Systems-centric:
      • Crash Hoare Logic

tenative schedule

Date Topic
Week of 1/13
  • Course Introduction
  • Hyperproperties [1]
Week of 1/20 No Class (POPL)
Week of 1/27
  • k-safety [1] and Self Composition [13]
  • Relational Program Logics [6]
Week of 2/3
  • Discussion: Cartesian Hoare Logic [9]
  • Probablistic Relational Hoare Logic [7]
Week of 2/10
  • Intro to Program Equivalence and Logical Relations [20, 23 (Chapter 6)]
  • Logical Relations, Continued [20, 23 (Chapter 6)]
Week of 2/17
  • Seminar: Jimmy Koppel: Building Multi-Language Tools
  • Parametricity [15]
Week of 2/24
  • Theorems for Free [16]
  • Seminar: Ankush Das: Resource-Aware Session Types for Digital Contracts.
Week of 3/02
  • Discussion: Step-Indexed Logical Relations [21]
  • Bisimulation and Trace Equivalence
Week of 3/09 Coinduction
Week of 3/16 No Class (Spring Break)
Week of 3/23 Corona Course Reboot
Week of 3/30
  • Intro to Consistency in Concurrent and Distributed Systems
    1. Designing Data-Intensive Applications. [Chapters 8+9]
    2. Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services. Seth Gilbert and Nancy Lynch.
    3. CAP Twelve Years Later: How the "Rules" Have Changed. Eric Brewer. [http]
  • Discussion [Guannan]: Automating the Choice of Consistency Levels in Replicated Systems. [33]
Week of 4/06
  • Discussion [Kia]: Declarative Programming over Eventually Consistent Data Stores. [28]
  • Discussion [Nitin]: 'Cause I'm Strong Enough: Reasoning About Consistency Choices in Distributed Systems. [31]
Week of 4/13
  • Discussion [Yuyan]: A Pragmatic Introduction to Secure Multi-Party Computation. [40, Chapters 1+2]
  • Discussion [Raghav]: SOK: General purpose compilers for secure multi-party computation. [41]
Week of 4/20
  • Discussion [Michael]: A model for delimited information release. [46]
  • Discussion [Qianchuan]: Wysteria: A programming language for generic, mixed-mode multiparty computations. [44]
Week of 4/27
  • Final Project Reports
  • Course Wrapup

bibliography

Hyperproperties

[1] Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157--1210, September 2010.
[2] Michael R Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K Micinski, Markus N Rabe, and César Sánchez. Temporal logics for hyperproperties. In International Conference on Principles of Security and Trust, pages 265--284. Springer, 2014.
[3] Norine Coenen, Bernd Finkbeiner, C�sar S�nchez, and Leander Tentrup. Verifying hyperliveness. pages 121--139, 07 2019. [ DOI ]
[4] Ron Shemer, Arie Gurfinkel, Sharon Shoham, and Yakir Vizel. Property Directed Self Composition, pages 161--179. 07 2019. [ DOI ]
[5] Azadeh Farzan and Anthony Vandikas. Automated Hypersafety Verification, pages 200--218. 07 2019. [ DOI ]

Relational Program Logics

[6] Nick Benton. Simple relational correctness proofs for static analyses and program transformations. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '04, pages 14--25, New York, NY, USA, 2004. ACM.
[7] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Formal certification of code-based cryptographic proofs. SIGPLAN Not., 44(1):90--101, January 2009. [Journal Version]
[8] Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub. A relational logic for higher-order programs. Proc. ACM Program. Lang., 1(ICFP):21:1--21:29, August 2017.
[9] Marcelo Sousa and Isil Dillig. Cartesian hoare logic for verifying k-safety properties. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '16, pages 57--69, New York, NY, USA, 2016. ACM.
[10] Kenji Maillard, Cătălin Hritcu, Exequiel Rivas, and Antoine Van Muylder. The next 700 relational program logics. Proceedings of the ACM on Programming Languages, 4(POPL):1--33, 2019.

Product Programs

[11] Gilles Barthe, Juan Manuel Crespo, and César Kunz. Beyond 2-safety: Asymmetric product programs for relational program verification. In International Symposium on Logical Foundations of Computer Science, pages 29--43. Springer, 2013.
[12] Gilles Barthe, Juan Manuel Crespo, and César Kunz. Relational verification using product programs. In Michael Butler and Wolfram Schulte, editors, FM 2011: Formal Methods, pages 200--214, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.
[13] Gilles Barth, Pedro R. D'Argenio, and Tamara Rezk. Secure information flow by self-composition. Mathematical Structures in Computer Science, 21(6):1207-1252, 2011.
[14] M�t� Kov�cs, Helmut Seidl, and Bernd Finkbeiner. Relational abstract interpretation for the verification of 2-hypersafety properties. pages 211--222, 11 2013.

Data Abstraction

[15] John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, pages 513--523, 1983. [ .pdf ]
[16] Philip Wadler. Theorems for free! In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA '89, page 347-359, New York, NY, USA, 1989. Association for Computing Machinery. [ bib | DOI | http ]
[17] John C. Mitchell and Gordon D. Plotkin. Abstract types have existential types. In Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '85, page 37-51, New York, NY, USA, 1985. Association for Computing Machinery. [ DOI | http ]
[18] William R. Cook. On understanding data abstraction, revisited. SIGPLAN Not., 44(10):557-572, October 2009. [ DOI | http ]
[19] C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1972. [ DOI ]
[20] Lau Skorstengaard. An introduction to logical relations. arXiv preprint arXiv:1907.11133, 2019. [http]
[21] Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657-inde683, September 2001. [ DOI | http ]
[22] Cyril Cohen, Maxime D�n�s, and Anders M�rtberg. Refinements for free! In Certified Programs and Proofs. Springer International Publishing, 2013.
[23] Benjamin C. Pierce. Advanced Topics in Types and Programming Languages. The MIT Press, 2004. [ bib ]

Refinement

[23] Edsger W. Dijkstra. A constructive approach to the problem of program correctness. Circulated privately, August 1967. [ .PDF ]
[24] J. He, C. A. R. Hoare, and J. W. Sanders. Data refinement refined. In Proc. ESOP, volume 213, pages 187--196. Springer Berlin Heidelberg, 1986. [ DOI ]
[25] Benjamin Delaware, Cl�ment Pit-Claudel, Jason Gross, and Adam Chlipala. Fiat: Deductive synthesis of abstract data types in a proof assistant. In Proc. POPL, pages 689--700. Association for Computing Machinery (ACM), 2015. [ DOI ]
[27] Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using crash hoare logic for certifying the fscq file system. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP '15, page 18-37, New York, NY, USA, 2015. Association for Computing Machinery. [ DOI | http ]

Consistency for Distributed Databases

[28] KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. Declarative Programming over Eventually Consistent Data Stores. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pages 413--424, New York, NY, USA, 2015. ACM. [ DOI | http ]
[29] Peter Alvaro, Neil Conway, Joe Hellerstein, and William R. Marczak. Consistency Analysis in Bloom: a CALM and Collected Approach. In CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings, pages 249--260, 2011.
[30] Peter Bailis, Alan Fekete, Michael J. Franklin, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. Coordination Avoidance in Database Systems. Proc. VLDB Endow., 8(3):185--196, November 2014. [ DOI | http ]
[31] Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 'Cause I'm Strong Enough: Reasoning About Consistency Choices in Distributed Systems. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pages 371--384, New York, NY, USA, 2016. ACM. [ DOI | http ]
[32] Valter Balegas, Nuno Preguiça, Rodrigo Rodrigues, Sérgio Duarte, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. Putting the Consistency back into Eventual Consistency. In Proceedings of the Tenth European Conference on Computer System, EuroSys '15, Bordeaux, France, 2015. [ .pdf ]
[33] Cheng Li, João Leitão, Allen Clement, Nuno Preguiça, Rodrigo Rodrigues, and Viktor Vafeiadis. Automating the Choice of Consistency Levels in Replicated Systems. In Proceedings of USENIX Annual Technical Conference, USENIX ATC'14, pages 281--292, Berkeley, CA, USA, 2014. USENIX Association. [ http ]
[34] Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguiça, and Rodrigo Rodrigues. Making Geo-replicated Systems Fast As Possible, Consistent when Necessary. In Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation, OSDI'12, pages 265--278, Berkeley, CA, USA, 2012. USENIX Association. [ http ]
[35] Mohsen Lesani, Christian J. Bell, and Adam Chlipala. Chapar: Certified Causally Consistent Distributed Key-value Stores. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 357--370, New York, NY, USA, 2016. ACM. [ DOI | http ]
[36] Gowtham Kaki, Kapil Earanky, KC Sivaramakrishnan, and Suresh Jagannathan. Safe replication through bounded concurrency verification. Proc. ACM Program. Lang., 2(OOPSLA):164:1--164:27, October 2018. [ DOI | http ]

Secure Information Flow

[37] John Mclean. A general theory of composition for a class of "possibilistic" properties. Software Engineering, IEEE Transactions on, 22:53 -- 67, 02 1996. [ DOI ]
[38] Geoffrey Smith. Principles of secure information flow analysis. In Mihai Christodorescu, Somesh Jha, Douglas Maughan, Dawn Song, and Cliff Wang, editors, Malware Detection, pages 291--307, Boston, MA, 2007. Springer US.
[39] Tachio Terauchi and Alex Aiken. Secure information flow as a safety problem. In Chris Hankin and Igor Siveroni, editors, Static Analysis, pages 352--367, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.

Secure Multiparty Computation

[40] David Evans, Vladimir Kolesnikov, and Mike Rosulek. A pragmatic introduction to secure multi-party computation. 2:70--246, 01 2018. [ DOI ]
[41] M. Hastings, B. Hemenway, D. Noble, and S. Zdancewic. SOK: General purpose compilers for secure multi-party computation. In 2019 IEEE Symposium on Security and Privacy (SP), pages 1220--1237, May 2019. [ DOI ]
[42] Florian Kerschbaum. Automatically optimizing secure computation. In Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS '11, page 703-714, New York, NY, USA, 2011. Association for Computing Machinery. [ DOI | http ]
[43] Aseem Rastogi, Piotr Mardziel, Michael Hicks, and Matthew A. Hammer. Knowledge inference for optimizing secure multi-party computation. In Proceedings of the Eighth ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS '13, page 3-14, New York, NY, USA, 2013. Association for Computing Machinery. [ DOI | http ]
[44] Aseem Rastogi, Matthew A. Hammer, and Michael Hicks. Wysteria: A programming language for generic, mixed-mode multiparty computations. In Proceedings of the 2014 IEEE Symposium on Security and Privacy, SP '14, page 655-670, USA, 2014. IEEE Computer Society. [ DOI | http ]
[45] Aseem Rastogi, Nikhil Swamy, and Michael Hicks. Wys*: A dsl for verified secure multi-party computations. In POST, 2018.
[46] Andrei Sabelfeld and Andrew C. Myers. A model for delimited information release. In Kokichi Futatsugi, Fumio Mizoguchi, and Naoki Yonezaki, editors, Software Security - Theories and Systems, pages 174--191, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.
[47] Samee Zahur and David Evans. Obliv-c: A language for extensible data-oblivious computation. IACR Cryptology ePrint Archive, 2015:1153, 2015.
[48] Kevin Liao, Matthew A. Hammer, and Andrew Miller. Ilc: A calculus for composable, computational cryptography. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, page 640-654, New York, NY, USA, 2019. Association for Computing Machinery. [ DOI | http ]
[49] Koki Hamada, Ryo Kikuchi, Dai Ikarashi, Koji Chida, and Katsumi Takahashi. Practically efficient multi-party sorting protocols from comparison sort algorithms. volume 7839, pages 202--216, 11 2012. [ DOI ]
[50] Koki Hamada, Dai Ikarashi, Koji Chida, and Katsumi Takahashi. Oblivious radix sort: An efficient sorting algorithm for practical secure multi-party computation. Cryptology ePrint Archive, Report 2014/121, 2014. https://eprint.iacr.org/2014/121.

Potpourri

[51] Yuepeng Wang, Xinyu Wang, and Isil Dillig. Relational program synthesis. Proc. ACM Program. Lang., 2(OOPSLA):155:1--155:27, October 2018.
[52] Vaughan R Pratt. Semantical consideration on floyo-hoare logic. In 17th Annual Symposium on Foundations of Computer Science (sfcs 1976), pages 109--121. IEEE, 1976.