- talks - lists.cs.princeton.edu

Katherine Edwards will present her FPO, "On edge colouring, fractionally colouring and partitioning graphs" on Tuesday, 5/31/2016 at 11am in CS 402
by Nicki Gotsis 18 May '16

18 May '16

Katherine Edwards will present her FPO "On edge colouring, fractionally colouring and partitioning graphs" on Tuesday, 5/31/2016 at 11am, 402 Computer Science Building. The members of her committee are Paul Seymour (adviser), Readers: Maria Chudnovsky (Math) and Chun-Hung Liu (Math); Nonreaders: Robert Tarjan and Bernard Chazelle. A copy of her thesis is available in Room 310. Everyone is invited to attend her talk. The abstract follow below. Abstract: We present an assortment of results in graph theory. First, Tutte conjectured that every two-edge connected cubic graph with no Petersen graph minor is three-edge-colourable. This generalizes the four-colour theorem. Robertson et al. had previously shown that to prove Tutte’s conjecture, it was enough to prove it for doublecross graphs. We provide a proof of the double cross case. Seymour conjectured the following generalization of the four-colour theorem. Every d-regular planar graph can be d-edge-coloured, provided that for every odd-cardinality set X of vertices, there are at least d edges with exactly one end in X. Seymour’s conjecture was previously known to be true for values of d  7. We provide a proof for the case d = 8. We then discuss upper bounds for the fractional chromatic number of graphs not containing large cliques. It has been conjectured that each graph with maximum degree at most ! and no complete subgraph of size ! has fractional chromatic number bounded below ! by at least a constant f(!). We provide the currently best known bounds for f(!), for 4  !  103. We also give a general upper bound for the fractional chromatic number in terms of the sizes of cliques and maximum degrees in local areas of a graph. Next, we give a result that says, roughly, that a graph with su"ciently large treewidth contains many disjoint subgraphs with ‘good’ linkedness properties. A similar result was a key tool in a recent proof of a polynomial bound in the excluded grid theorem. Our theorem is a quantitative improvement with a new proof. Finally, we discuss the p-centre problem, a central NP-hard problem in graph clustering. Here we are given a graph and an integer p, and need to identify a set of p vertices, called centres, so that the maximum distance from a vertex to its closest centre (the p-radius) is minimized. We give a quasilinear time approximation algorithm to solve p-centres when the hyperbolicity of the graph is fixed, with a small additive error on the p-radius.

1 0

Talk: June Andronick today, 10:30am
by Nicole E. Wagenblast 16 May '16

16 May '16

Talk: Interrupts in OS code: let’s reason about them. Yes, this means concurrency. June Andronick, Data61 Monday, May 16th, 10:30am Computer Science 402 Existing modelled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions. In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task. June Andronick is a Senior Researcher at Data61|CSIRO (formerly NICTA). Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She contributed to the seL4 correctness proof and now focuses on concurrency reasoning for OS code. She leads the concurrency software verification research in Data61, and is deputy leader of the Trustworthy Systems group. She was recognised in 2011 by MIT's Technology Review as one of the world's top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.

1 0

Talk: June Andronick Monday May 16, 10:30am- reminder
by Nicole E. Wagenblast 15 May '16

15 May '16

Talk: Interrupts in OS code: let’s reason about them. Yes, this means concurrency. June Andronick, Data61 Monday, May 16th, 10:30am Computer Science 402 Existing modelled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions. In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task. June Andronick is a Senior Researcher at Data61|CSIRO (formerly NICTA). Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She contributed to the seL4 correctness proof and now focuses on concurrency reasoning for OS code. She leads the concurrency software verification research in Data61, and is deputy leader of the Trustworthy Systems group. She was recognised in 2011 by MIT's Technology Review as one of the world's top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.

1 0

CORRECTION: Laura Roberts will present her general exam on Wednesday, May 18, 2016 at 2pm in CS 402.
by Nicki Gotsis 12 May '16

12 May '16

CORRECTION: The members of Laura Roberts committee are Nick Feamster (adviser), Jennifer Rexford, and Arvind Narayanan. ________________________ > On May 12, 2016, at 9:06 AM, Nicki Gotsis <ngotsis(a)CS.Princeton.EDU> wrote: > > Laura Roberts will present her general exam on Wednesday, May 18, 2016 at 2pm in CS 402. > > The members of her committee are Jennifer Rexford (adviser), Nick Feamster, and Arvind Narayanan. > > Everyone is invited to attend her talk, and those faculty wishing to remain for the oral exam following are welcome to do so. Her abstract and reading list follow below. > > Abstract: > Tor is a very popular anonymity network that is known to be susceptible to end-to-end traffic correlation attacks that can be performed by network-level adversaries such as ASes and IXPs. Previous work on such attacks has focused on the TCP streams while the accompanying DNS traffic has been completely ignored. In our work we study the nature of DNS resolution in Tor and how DNS traffic can be used by network-level adversaries to deanonymize Tor traffic. For example, we are investigating how DNS traffic can be used to boost the success of website fingerprinting attacks. Our contributions include drawing attention to the role DNS can play in Tor deanonymization attacks and improving upon earlier Tor measurement techniques in order to produce results and estimates that are more practical and realistic. > > Reading List: > - Computer Networks (5th edition) by Tanenbaum and Wetherall, Chs. 1, 5-8 > - Security Engineering: A Guide to Building Dependable Distributed Systems by Anderson, Chs. 1-8, 21-24 > - “Tor: The Second-Generation Onion Router” by Dingledine et al. > - “Users Get Routed: Traffic Correlation on Tor by Realistic Adversaries” by Johnson et al. > - “Location Diversity in Anonymity Networks” by Feamster and Dingledine > - “Website Fingerprinting at Internet Scale” by Panchenko et al. > - “A Critical Evaluation of Website Fingerprinting Attacks” by Juarez et al. > - “Passive Attack Analysis for Connection-Based Anonymity Systems” by Serjantov and Sewell > - “Defending Tor from Network Adversaries: A Case Study of Network Path Prediction” by Juen et al. > - “AS-awareness in Tor Path Selection” by Edman and Syverson > - “DNS measurements at a root server” by Brownlee et al. > - “Sampled Traffic Analysis by Internet-Exchange-Level Adversaries” by Murdoch and Zieliński > _______________________________________________ > talks mailing list > talks(a)lists.cs.princeton.edu > To edit subscription settings or remove yourself, use this link: > https://lists.cs.princeton.edu/mailman/listinfo/talks

1 1

Laura Roberts will present her general exam on Wednesday, May 18, 2016 at 2pm in CS 402.
by Nicki Gotsis 12 May '16

12 May '16

Laura Roberts will present her general exam on Wednesday, May 18, 2016 at 2pm in CS 402. The members of her committee are Jennifer Rexford (adviser), Nick Feamster, and Arvind Narayanan. Everyone is invited to attend her talk, and those faculty wishing to remain for the oral exam following are welcome to do so. Her abstract and reading list follow below. Abstract: Tor is a very popular anonymity network that is known to be susceptible to end-to-end traffic correlation attacks that can be performed by network-level adversaries such as ASes and IXPs. Previous work on such attacks has focused on the TCP streams while the accompanying DNS traffic has been completely ignored. In our work we study the nature of DNS resolution in Tor and how DNS traffic can be used by network-level adversaries to deanonymize Tor traffic. For example, we are investigating how DNS traffic can be used to boost the success of website fingerprinting attacks. Our contributions include drawing attention to the role DNS can play in Tor deanonymization attacks and improving upon earlier Tor measurement techniques in order to produce results and estimates that are more practical and realistic. Reading List: - Computer Networks (5th edition) by Tanenbaum and Wetherall, Chs. 1, 5-8 - Security Engineering: A Guide to Building Dependable Distributed Systems by Anderson, Chs. 1-8, 21-24 - “Tor: The Second-Generation Onion Router” by Dingledine et al. - “Users Get Routed: Traffic Correlation on Tor by Realistic Adversaries” by Johnson et al. - “Location Diversity in Anonymity Networks” by Feamster and Dingledine - “Website Fingerprinting at Internet Scale” by Panchenko et al. - “A Critical Evaluation of Website Fingerprinting Attacks” by Juarez et al. - “Passive Attack Analysis for Connection-Based Anonymity Systems” by Serjantov and Sewell - “Defending Tor from Network Adversaries: A Case Study of Network Path Prediction” by Juen et al. - “AS-awareness in Tor Path Selection” by Edman and Syverson - “DNS measurements at a root server” by Brownlee et al. - “Sampled Traffic Analysis by Internet-Exchange-Level Adversaries” by Murdoch and Zieliński

1 0

Paul Ellenbogen will present his general exam on Wednesday, May 18, 2016 at 10:15am in CS 302.
by Nicki Gotsis 11 May '16

11 May '16

Paul Ellenbogen will present his general exam on Wednesday, May 18, 2016 at 10:15am in CS 302. The members of his committee are Arvind Narayanan (adviser), Barbara Engelhardt, and Prateek Mittal. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. ABSTRACT: DNA fingerprinting is the practice of mapping unidentified genetic material to its owner. Currently deployed DNA fingerprinting techniques utilize only a small amount of the information available in human genome, and leverage none of the existing genealogical information. The only other work that has attempted to use genealogical information is limited to inferring the surnames of males, using the heuristic that the surname is correlated with the Y chromosome. We present the first general algorithm for DNA fingerprinting using a small set (~1% of the population) of known genomes in combination with comprehensive genealogical information. With genealogical data and recombination data from the HapMap project, we can repeatedly simulate a pair of individuals’ genomes, allowing us to learn the distribution of shared genetic material between the pair. Using strong independence assumptions and the simulation-generated distributions, we can estimate the joint distribution of shared genetic material for any individual’s genome compared against a set of individuals with known genomes. Unknown genomes can then be matched with their owner by calculating the amount of shared genetic material with each of the known genomes, and picking the individual whose joint distribution predicts the highest probability for that amount of shared genetic material. Thus, we are able to identify individuals using a relatively small number of genomes. This has privacy implications, as it shows that an individual releasing their genetic data may compromise the privacy of their relatives. READING LIST: Book: Hartl, Daniel L., and A. G. Clark. "Principles of Population Genetics (Sinauer, Sunderland, MA)." *the text* (2007). Chapters 2.1, 2.2, 2.5-2.7, 6, 9.2, 1 Articles: 1. Malin, Bradley. "Re-identification of familial database records." *AMIA*. 2006. 2. Homer, Nils, et al. "Resolving individuals contributing trace amounts of DNA to highly complex mixtures using high-density SNP genotyping microarrays." *PLoS Genet* 4.8 (2008): e1000167. 3. Joh, Elizabeth E. "DNA Theft: Recognizing the Crime on Nonconsensual Genetic Collection and Testing." *BUL Rev.* 91 (2011): 665. 4. Durand, Eric Y., Nicholas Eriksson, and Cory Y. McLean. "Reducing pervasive false-positive identical-by-descent segments detected by large-scale pedigree analysis." *Molecular biology and evolution* (2014): msu151. 5. Humbert, Mathias, et al. "De-anonymizing Genomic Databases Using Phenotypic Traits." *Proceedings on Privacy Enhancing Technologies* 2015.2 (2015): 99-114. 6. Manichaikul, Ani, et al. "Robust relationship inference in genome-wide association studies." *Bioinformatics* 26.22 (2010): 2867-2873. 7. Palamara, Pier Francesco, et al. "Length distributions of identity by descent reveal fine-scale demographic history." *The American Journal of Human Genetics* 91.5 (2012): 809-822. 8. Joh, Elizabeth E. "Reclaiming'Abandoned'DNA: The Fourth Amendment and Genetic Privacy." *Northwestern University Law Review* 100 (2006): 857. 9. Gymrek, Melissa, et al. "Identifying personal genomes by surname inference." *Science* 339.6117 (2013): 321-324. 10. Humbert, Mathias, et al. "Addressing the concerns of the lacks family: quantification of kin genomic privacy." *Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security*. ACM, 2013. 11. Sweeney, Latanya, Akua Abu, and Julia Winn. "Identifying participants in the personal genome project by name." *Available at SSRN 2257732* (2013).

1 0

Jonathan Zung will present his general exam on Wednesday, May 18, 2016 at 4pm in CS 402.
by Nicki Gotsis 11 May '16

11 May '16

Jonathan Zung will present his general exam on Wednesday, May 18, 2016 at 4pm in CS 402. The members of his committee are Sebastian Seung (adviser), Tom Funkhouser, and Szymon Rusinkiewicz. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. Bishop, Christopher M. "Pattern Recognition." Machine Learning (2006). Szeliski, Richard. Computer vision: algorithms and applications. Springer Science & Business Media, 2010. Arbelaez, Pablo, et al. "Contour detection and hierarchical image segmentation." Pattern Analysis and Machine Intelligence, IEEE Transactions on 33.5 (2011): 898-916. Wirjadi, Oliver. Survey of 3d image segmentation methods. Vol. 35. ITWM, 2007. Yang, Mingqiang, Kidiyo Kpalma, and Joseph Ronsin. "A survey of shape feature extraction techniques." Pattern recognition (2008): 43-90. Briggman, Kevin, et al. "Maximin affinity learning of image segmentation." Advances in Neural Information Processing Systems. 2009. Jain, Viren, et al. "Learning to agglomerate superpixel hierarchies." Advances in Neural Information Processing Systems. 2011. Bogovic, John A., Gary B. Huang, and Viren Jain. "Learned versus hand-designed feature representations for 3d agglomeration." arXiv preprint arXiv:1312.6159 (2013). Lee, Honglak, et al. "Convolutional deep belief networks for scalable unsupervised learning of hierarchical representations." Proceedings of the 26th Annual International Conference on Machine Learning. ACM, 2009. Long, Jonathan, Evan Shelhamer, and Trevor Darrell. "Fully convolutional networks for semantic segmentation." Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 2015. Noh, Hyeonwoo, Seunghoon Hong, and Bohyung Han. "Learning deconvolution network for semantic segmentation." Proceedings of the IEEE International Conference on Computer Vision. 2015. Kumar, M. Prema, P. H. S. Ton, and Andrew Zisserman. "Obj cut." Computer Vision and Pattern Recognition, 2005. CVPR 2005. IEEE Computer Society Conference on. Vol. 1. IEEE, 2005. Borenstein, Eran, and Shimon Ullman. "Combined top-down/bottom-up segmentation." Pattern Analysis and Machine Intelligence, IEEE Transactions on 30.12 (2008): 2109-2125. Yang, Yi, et al. "Layered object models for image segmentation." Pattern Analysis and Machine Intelligence, IEEE Transactions on 34.9 (2012): 1731-1743. Abstract: My research has been motivated by the problem of segmenting 3d electron microscopy images of brain tissue in order to reconstruct neural circuits. Such images require instance level segmentation (we want to label each individual neuron separately) and are extremely cluttered (the image is densely filled with cells). The gap between human and machine performance on this task seems to lie in the ability of humans to focus on individual objects and make use of priors on their shapes. State of the art techniques for this problem rely on supervised deep neural networks to perform boundary detection. I will present an approach to augmenting such networks with an attentional mechanism with the goal of forcing the network to focus on a single object at a time, thereby allowing better use of priors on the shapes of individual objects.

1 0

Harry Kalodner will present his general exam on Tuesday, May 17, 2016 at 12pm in CS 302.
by Nicki Gotsis 10 May '16

10 May '16

Harry Kalodner will present his general exam on Tuesday, May 17, 2016 at 12pm in CS 302. The members of his committee are Arvind Narayanan (adviser), Nick Feamster, and Aarti Gupta. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. ABSTRACT Bitcoin, initially designed as a system for the issuance and transfer of electronic cash, provides a foundation for the construction of complex and powerful applications. The underlying technology of Bitcoin, the blockchain, is a powerful tool to secure information and coordinate exchanges between mutually distrustful parties. New methods of analysis and system design must be developed to understand and make take advantage of these tools. Namecoin is a cryptocurrency modeled after Bitcoin which implements a decentralized alternative to DNS. The public nature of blockchain technology provides direct visibility into how the system is used in practice. I discuss a number of techniques used to analyze the use and function of Namecoin. I then discuss some major pitfalls of Namecoin’s design and lessons that can be learned in the development of future systems. Taking lessons from the design of Namecoin, I describe a proposed system, IPCoin, designed to replace the centralized structure of the RPKI. Currently a core group of central entities hold the power to disrupt the routing of packets on the internet. IPCoin provides a method of removing this centralization, thus minimizing the attack surface available for disrupting core functionality of the internet. IPCoin provides a system for the fair distribution of IP address ranges, the ability to securely control these ranges, and the easy auditing of the global consensus state of the system. Reading List: Books: Ross J. Anderson. 2008. Security Engineering: A Guide to Building Dependable Distributed Systems (2 ed.). Wiley Publishing. (Chapters 5, 6, 7, 10, 21) Larry L. Peterson and Bruce S. Davie. 2011. Computer Networks, Fifth Edition: A Systems Approach (5th ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. (Chapters 1,2,3,4) Arvind Narayanan. 2016. Bitcoin and Cryptocurrency Technologies. (Chapters 2, 3, 9, 10, 11) Papers: 1. Bitcoin: Nakamoto, Satoshi. "Bitcoin: A peer-to-peer electronic cash system." Joseph Bonneau, Andrew Miller, Jeremy Clark, Arvind Narayanan, Joshua A. Kroll, Edward W. Felten. "Research Perspectives and Challenges for Bitcoin and Cryptocurrencies.” IEEE Security & Privacy, 2015. Jeremy Clark, Joseph Bonneau, Edward W. Felten, Joshua A. Kroll, Andrew Miller, Arvind Narayanan. "On Decentralizing Prediction Markets and Order Books." WEIS 2014. Sarah Meiklejohn, Marjoir Pomarole, Grant Jordan, Kirill Levchenko, Damon McCoy, Geoffrey M. Voelker, Stefan Savage. "A fistful of bitcoins: Characterizing payments among men with no names." In Proceedings of the ACM Internet Measurement Conference (IMC), pages 127–140, New York, 2013. ACM Muneeb Ali, Jude Nelson, Ryan Shea, Michael J. Freedman. "Blockstack: Design and Implementation of a Global Naming System with Blockchains.” To appear in USENIX ATC’16. Meni Rosenfeld. "Overview of colored coins." http://bitcoil.co.il/BitcoinX.pdf, December 2012. 2. BGP and RPKI K. Butler, T. Farley, P. McDaniel and J. Rexford. "A survey of BGP security issues and solutions." Proc. IEEE, vol. 98, no. 1, pp. 100-122, 2010 M. Lepinski and S. Kent, “An Infrastructure to Support Secure Internet Routing,” IETF, RFC 6480, February 2012. Danny Cooper , Ethan Heilman , Kyle Brogle , Leonid Reyzin , Sharon Goldberg. "On the risk of misbehaving RPKI authorities." Proceedings of the Twelfth ACM Workshop on Hot Topics in Networks, p.1-7, November 21-22, 2013. College Park, Maryland Ethan Heilman , Danny Cooper , Leonid Reyzin , Sharon Goldberg. "From the consent of the routed: improving the transparency of the RPKI." Proceedings of the 2014 ACM conference on SIGCOMM, August 17-22, 2014, Chicago, Illinois, USA

1 0

Yida Wang will present his FPO, " Large-scale analyses of functional interactions in the human brain" on Tuesday, 5/17/2016 at 3:00PM in A32 Peretsman-Scully Hall.
by Nicki Gotsis 10 May '16

10 May '16

Yida Wang will present his FPO," Large-scale analyses of functional interactions in the human brain" on Tuesday, 5/17/2016 at 3:00PM in A32 Peretsman-Scully Hall. The members of his committee are Kai Li (adviser), readers: Jon Cohen and Nick Turk-Browne; nonreaders: Olga Troyanskaya and Sebastian Seung. A copy of his thesis is available in Room 310. Everyone is invited to attend his talk. The talk abstract follow below. Abstract: A grand challenge in neuroscience is to understand how a human brain functions. Much previous research has focused on studying the activities of brain regions. However, the functional interactions between brain regions are not well understood. This dissertation focuses on computational methods to analyze data from functional magnetic resonance imaging (fMRI) scanners to study the functional interactions in the human brain. This dissertation proposes, designs and implements efficient systems to conduct full correlation matrix analysis (FCMA) as an unbiased way to explore functional interactions in the human brain. Since a straightforward way to study FCMA would take years to complete one run with a typical neuroscience study dataset on a modern compute server, no previous attempt has been made in the past. This dissertation makes several contributions. First, we proposed and implemented parallel algorithms and optimizations on a multi-processor cluster, which improved FCMA computation by three orders of magnitude. Second, we demonstrated that FCMA can effectively show functional interactions in the human brain by conducting a neuroscience study on an fMRI dataset. Our study successfully identified functional interactions between certain brain regions. Third, we proposed and implemented optimization methods for FCMA for emerging many-core processors such as the Intel Xeon Phi coprocessors and improved the performance of computing FCMA by another order of magnitude. On a 96-node Xeon Phi cluster, our system can finish an FCMA study with a typical dataset in minutes. Finally, we proposed, designed and implemented a service for real-time, closed loop neuroscience studies. Our real-time FCMA can process and analyze brain volumes from multiple fMRI experiments on a 40-node compute cluster simultaneously and send the neurofeedback to each fMRI scanner over the Internet within 1.5 seconds. This system uses a novel method to improve the performance and utilization of compute nodes while meeting the real-time requirements in the presence of node failures.

1 0

Talk: June Andronick Monday May 16, 11:00am
by Nicole E. Wagenblast 10 May '16

10 May '16

Talk: Interrupts in OS code: let’s reason about them. Yes, this means concurrency. June Andronick, Data61 Monday, May 16th, 11:00am Computer Science 105 Existing modelled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions. In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task. June Andronick is a Senior Researcher at Data61|CSIRO (formerly NICTA). Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She contributed to the seL4 correctness proof and now focuses on concurrency reasoning for OS code. She leads the concurrency software verification research in Data61, and is deputy leader of the Trustworthy Systems group. She was recognised in 2011 by MIT's Technology Review as one of the world's top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.

1 0