Bangalore Systems Reading Group

Announcement email

We plan to start a systems reading group at IISc. Every week we will discuss papers from top systems, security, and PL conferences. We will run this like a seminar course. Every week one volunteer from the group will prepare and present the paper for 25 minutes, and then lead a discussion on the paper. We expect to discuss papers that span across topics in systems, security, PL, and formal methods. The proposed list of papers is given below. Please reply to Arvind Seshadri <asesdri@gmail.com> if you would like to be deleted from this group, or wish to add other colleagues of yours that are interested in attending. The reading group will be held at CSA Room 252 from 3:30-4:30 PM every Thursday. The first meeting will be on Thursday, August 13th.

Reading List Schedule

DatePaperPresenter
July 21, 2016 B. Kellogg, V. Talla, S. Gollakota, J. Smith, Passive Wi-Fi: Bringing Low Power to Wi-Fi Transmissions, NSDI 2016 (Best Paper Award) Sorav Bansal (IITD/IISc)
June 30, 2016 Discussion on papers at ASPLOS 2016 continued Aravinda Prasad (IISc)
June 23, 2016 Discussion on papers at ASPLOS 2016 continued Rupesh Wani (IISc)
June 16, 2016 Discussion on papers at ASPLOS 2016 continued Aravinda Prasad (IISc)
June 2, 2016 Discussion on papers at ASPLOS 2016 Aravinda Prasad (IISc)
May 12, 2016 Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, Armando Solar-Lezama, "Towards optimization-safe systems: analyzing the impact of undefined behavior", SOSP 2013 Sorav Bansal (IITD/IISc)
April 21, 2016 C. Rossbach, Y. Yu, J. Currey, J.P. Martin, D. Fetterly, Dandelion: a Compiler and Runtime for Heterogeneous Systems, SOSP 2013 Sorav Bansal (IITD/IISc)
March 31, 2016 Alex Kogan, Erez Petrank, papers on wait-free data structures (PPoPP11, PPoPP12) Priyanka Singla (IISc)
March 24, 2016 Prudent Memory Reclamation in Procrastination-based Synchronization, ASPLOS 2016 practice talk Aravinda Prasad (IISc/IBM)
March 17, 2016 A sampling of this year's FAST papers Suparna Bhattacharya (HP Labs)
March 10, 2016 The Click modular router (paper1, paper2, paper3) Sorav Bansal (IITD/IISc)
March 3, 2016 Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock, JitK: A Trustworthy In-Kernel Interpreter Infrastructure, OSDI 2014 Ashwin (IISc)
Feb. 18, 2016 Changwoo Min, Sanidhya Kashyap, Byoungyoung Lee, Chengyu Song, Taesoo Kim, Cross-checking Semantic Correctness: The Case of Finding File System Bugs, SOSP 2015 Arpith (IISc)
Feb. 4, 2016 Lu Fang, Khanh Nguyen, Guoqing Xu, Brian Demsky, Shan Lu, Interruptible Tasks: Treating Memory Pressure As Interrupts for Highly Scalable Data-Parallel Programs, SOSP 2015 Naman Patel (IISc)
Jan. 14, 2016 Tudor David, Rachid Guerraoui, Vasileios Trigonakis, Everything You Always Wanted to Know About Synchronization but Were Afraid to Ask, SOSP 2013 Deepak Ravi (IITD)
Jan. 7, 2016 Dependability in a Connected World: From the Very Large to the Very Small Saurabh Bagchi (Purdue Univ.)
Dec. 24, 2015 Mihai Dobrescu, Norbert Egi, Katerina Argyraki, Byung-Gon Chun, Kevin Fall, Gianluca Iannaccone, Allan Knies, Maziar Manesh, and Sylvia Ratnasamy, RouteBricks: exploiting parallelism to scale software routers, SOSP 2009 Shashank Khasare (IITD)
Dec. 17, 2015 Charlie Curtsinger, Emery D. Berger, Coz: Finding Code that Counts with Causal Profiling, SOSP 2015 Malavika Samak (IISc)
Dec. 11, 2015 Modular Programming for Reliable Distributed Systems Shaz Qadeer (Microsoft Research)
Dec. 10, 2015 Persistent Memory Programming - Progress and Frontiers Doug Voigt (HP Enterprise Storage Division)
Dec. 3, 2015 Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazieres, Making Information Flow Explicit in HiStar, OSDI 2006. Sorav Bansal (IITD/IISc)
Nov. 5, 2015 M. Zaharia, T. Das, H. Li, T. Hunter, S. Shenker, and I. Stoica. Discretized Streams: Fault-Tolerant Streaming Computation at Scale, SOSP 2013. Kaushik Rajan (Microsoft Research)
Oct. 29, 2015 Jelle van den Hooff, David Lazar, Matei Zaharia, and Nickolai Zeldovich, Vuvuzela : Scalable Private Messaging Resistant to Traffic Analysis , SOSP 2015 Rupesh Wani (IISc)
Oct. 15, 2015 Haonan Lu, Kaushik Veeraraghavan, Philippe Ajoux, Jim Hunt, Yee Jiun Song, Wendy Tobagus, Sanjeev Kumar, Wyatt Lloyd, Existential Consistency: Measuring and Understanding Consistency at Facebook, SOSP 2015. Priyanka Singla (IISc)
Oct. 8, 2015 Alexander Matveev, Nir Shavit, Pascal Felber, Patrick Marlier, "Read-Log-Update: A Lightweight Synchronization Mechanism for Concurrent Programming", SOSP 2015. Aravinda Prasad (IISc)
Oct. 1, 2015 Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich, Using Crash Hoare Logic for Certifying the FSCQ File System, SOSP 2015. Sorav Bansal (IITD/IISc)
Sep. 24, 2015 Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, Brian Zill, IronFleet: Proving Practical Distributed Systems Correct, SOSP 2015. Akash Lal (Microsoft Research)
Sep. 3, 2015 Chang Liu, Austin Harris, Martin Maas, Michael W. Hicks, Mohit Tiwari, Elaine Shi, GhostRider: A Hardware-Software System for Memory Trace Oblivious Computation, ASPLOS 2015 Satish Narayanasamy (U. Michigan)
Aug. 27, 2015 Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood, seL4: Formal Verification of an OS Kernel Sorav Bansal (IITD/IISc)
Aug. 20, 2015 Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Microsoft Research; Arjun Narayan, University of Pennsylvania; Bryan Parno, Microsoft Research; Danfeng Zhang, Cornell University; Brian Zill, Microsoft Research. Ironclad Apps: End-to-End Security via Automated Full-System Verification, OSDI 2014 Arvind Seshadri (IBM Research)
Aug. 13, 2015 Veselin Raychev, Madanlal Musuvathi, Todd Mytkowicz, "Parallelizing user-defined aggregations using symbolic execution", to appear in SOSP 2015. Sriram Rajamani (Microsoft Research)

Mailing List

http://mailman.serc.iisc.in/mailman/listinfo/sys-seminar

Tentative List of Papers

Systems and formal methods papers accepted to SOSP 2015:
  1. Using Crash Hoare Logic for Certifying the FSCQ File System, Haogang Chen, Daniel Ziegler, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich (MIT CSAIL)
  2. SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems, Tom Ridge (University of Leicester), David Sheets (University of Cambridge), Thomas Tuerk (FireEye), Anil Madhavapeddy (University of Cambridge), Andrea Giugliano (University of Leicester), and Peter Sewell (University of Cambridge)
  3. Failure Sketching: A Technique for Automated Root Cause Diagnosis of In-Production Failures, Baris Kasikci and Benjamin Schubert (EPFL), Cristiano Pereira and Gilles Pokam (Intel Corporation), and George Candea (EPFL)
  4. Parallelizing user-defined aggregations using symbolic execution, Veselin Raychev (ETH Zurich) and Madanlal Musuvathi and Todd Mytkowicz (Microsoft Research)
  5. Cross-checking Semantic Correctness: The Case of Finding File System Bugs, Changwoo Min, Sanidhya Kashyap, Byoungyoung Lee, Chengyu Song, and Taesoo Kim (Georgia Institute of Technology)
  6. Scalable Private Messaging Resistant to Traffic Analysis, Jelle van den Hooff, David Lazar, Matei Zaharia, and Nickolai Zeldovich (MIT)
  7. No compromises: distributed transactions with consistency, availability and performance, Aleksandar Dragojevic, Dushyanth Narayanan, Ed Nightingale, Matthew Renzelmann, Alex Shamis, Anirudh Badam, and Miguel Castro (Microsoft Research)
Recent papers on formally-verified systems:
  1. Ironclad Apps: End-to-End Security via Automated Full-System Verification (OSDI 2014) Authors: Chris Hawblitzel, Jon Howell, and Jacob R. Lorch, Microsoft Research; Arjun Narayan, University of Pennsylvania; Bryan Parno, Microsoft Research; Danfeng Zhang, Cornell University; Brian Zill, Microsoft Research
  2. Formal verification of information flow security for a simple arm-based separation kernel (CCS 2013) Authors: M. Dam, R. Guanciale, N. Khakpour, H. Nemati, and O. Schwarz
  3. seL4: From general purpose to a proof [61] of information flow enforcement (IEEE S&P 2013) Authors: T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein
  4. seL4: Formal verification of an OS kernel (SOSP 2009) Authors: G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, M. Norrish, R. Kolanski, T. Sewell, H. Tuch, and S. Winwood
Papers of historical importance (in no particular order):
  1. Noninterference, transitivity, and channel-control security policies (SRI technical report) Author: John Rushby Significance: Introduces intransitive noninterference
  2. Design and Verification of Secure Systems (SOSP 1981) Author: John Rushby Significance: Introduces the notion of a separation kernel
  3. A retrospective on the VAX VMM security kernel. IEEE Transactions on Software Engineering, 17(11):1147–1165, Nov. 1991 Authors: P. A. Karger, M. E. Zurko, D. W. Bonin, A. H. Mason, and C. E. Kahn Significance: The first commodity VMM to receive an A1 Orange Book Rating
  4. An analysis of covert timing channels (IEEE S&P 1991) Author: John Wray Significance: Argures that it is not possible to classify a covert channel as a timing or a storage channel