Principal Scientist
Stealth Software Technologies, Inc.
david@stealthsoftwareinc.com
@daviddarais
@davdar
CV
I'm a Principal Scientist at Stealth Software Technologies. I was previously a Principal Scientist at Galois.
I lead business development and engineering teams that perform on science and engineering programs funded by the US Government.
My research focuses on software reliability and data privacy through advances in program analysis, symbolic model checking, computer-checkable proofs, secure multiparty computation, zero knowledge proofs, oblivious data structures, differential privacy verification and differential privacy standards.
I used to help run and still actively collaborate with the UVM PLAID Lab.
Publications
(This list is out of date... see my dblp)-
Zero Knowledge Static Program Analysis.
Zhiyong Fang, David Darais, Joe Near, Yupeng Zhang.
To appear in Computer and Communications Security (CCS). ACM, 2021.
[pdf] [abstract] -
Solo: Enforcing Differential Privacy Without Fancy Types.
Chike Abuah, David Darais, Joe Near.
Foundations of Computer Security (FCS). 2021.
-
Symphony: A Concise Language Model for MPC.
Ian Sweet, Ryan Estes, David Darais, David Heath, William Harris, Michael Hicks.
Foundations of Computer Security (FCS). 2021.
-
Verified Computation via Compilation to Abstract Machines.
Ryan Estes, David Darais, Joseph Near.
Foundations of Computer Security (FCS). 2021.
[pdf] [abstract] -
DDUO: General-Purpose Dynamic Analysis for Differential Privacy.
Chike Abuah, Alex Silence, David Darais, Joseph P. Near.
Computer Security Foundations (CSF). IEEE, 2021.
[pdf] -
Improving Privacy-Preserving Deep Learning With Immediate Sensitivity.
Timothy Stevens, David Darais, Ben U Gelman, David Slater, Joseph Near.
Theory and Practice of Differential Privacy (TPDP). 2021.
-
Solo: Enforcing Differential Privacy Without Fancy Types.
Chike Abuah, David Darais, Joe Near.
Theory and Practice of Differential Privacy (TPDP). 2021.
-
DuetSGX: Differential Privacy with Secure Hardware.
Phillip Nguyen, Alex Silence, David Darais, Joseph P. Near.
Theory and Practice of Differential Privacy (TPDP). 2020.
[pdf] [abstract] [bibtex] [arXiv] -
Short Paper: Probabilistically Almost-Oblivious Computation.
Ian Sweet, David Darais, Michael Hicks.
Programming Languages and Analysis for Security (PLAS). ACM, 2020.
[pdf] [abstract] [bibtex] [ACM] -
Types and Abstract Interpretation for Authorization Hook Advice.
Christian Skalka, David Darais, Trent Jaeger, Frank Capobianco.
Computer Security Foundations (CSF). IEEE, 2020.
[pdf] [abstract] [bibtex] [IEEE] -
Abstracting Faceted Execution.
Kristopher Micinski, David Darais, Thomas Gilray.
Computer Security Foundations (CSF). IEEE, 2020.
[pdf] [abstract] [bibtex] [IEEE] -
A Language for Probabilistically Oblivious Computation.
David Darais, Ian Sweet, Chang Liu, Michael Hicks.
Principles of Programming Languages (POPL). ACM, 2020.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.key] [slides.pdf] -
Proof Carrying Network Code.
Christian Skalka, John Ring, David Darais, Minseok Kwon, Sahil Gupta, Kyle Diller, Steffan Smolka, Nate Foster.
Computer and Communications Security (CCS). ACM, 2019.
[pdf] [abstract] [bibtex] [ACM] -
Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy.
Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, Dawn Song.
Object-oriented Programming, Systems, Languages, and Applications (OOPSLA). ACM, 2019.
«ACM SIGPLAN Distinguished Paper Award»
[pdf] [abstract] [bibtex] [ACM] [arXiv] [video] -
Constructive Galois Connections.
David Darais, David Van Horn.
Journal of Functional Programming (JFP). Cambridge University Press, 2019.
[pdf] [abstract] [bibtex] [JFP] [arXiv] -
Abstracting Definitional Interpreters.
David Darais, Nicholas Labich, Phúc C. Nguyễn, David Van Horn.
International Conference on Functional Programming (ICFP). ACM, 2017.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.
David Darais, David Van Horn.
International Conference on Functional Programming (ICFP). ACM, 2016.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Compositional and Mechanically Verified Program Analyzers.
David Darais.
ECOOP Doctoral Symposium (ECOOP-DS). 2016.
[pdf] [abstract] [slides.pdf] [slides.key] -
Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis.
David Darais, Matthew Might, David Van Horn.
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA). ACM, 2015.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Monadic Abstract Interpreters.
Ilya Sergey, Dominique Divriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens.
Programming Language Design and Implementation (PLDI). ACM, 2013.
[pdf] [abstract] [bibtex] [ACM] -
Macros that Work Together: Compile-time Bindings, Partial Expansion, and Definition Contexts.
Matthew Flatt, Ryan Culpepper, David Darais, Robert Bruce Findler.
Journal of Functional Programming (JFP). Cambridge University Press, 2012.
[pdf] [abstract] [bibtex] [ACM] -
Functional Pearl: Parsing with Derivatives.
Matthew Might, David Darais, Daniel Spiewak.
International Conference on Functional Programming (ICFP). ACM, 2011.
[pdf] [abstract] [bibtex] [ACM]
Theses
-
Mechanizing Abstract Interpretation.
David Darais.
PHD Thesis. University of Maryland. 2017.
[pdf] [abstract] [slides.pdf] [slides.key]
Drafts
-
The Final Pretty Printer.
David Christiansen, David Darais, Weixi Ma.
Draft. May 2017.
[pdf] [abstract]
Talks
-
Data-oblivious Computation.
Hot Topics in the Science of Security (HotSoS) Symposium - Hard Problems Special Session. Virtual. April, 2021.
[HotSoS] [abstract] [slides.pdf] [slides.key] -
Data Privacy by Programming Language Design.
Tech Talk - Millennium Institute - Foundational Research on Data. University of Chile, Santiago, Chile. May, 2019.
[UChile] [IMFD] [abstract] [slides.pdf] [slides.key] -
A Simple and Extensible Approach to Program Analysis.
International Federation for Information Processing Working Group 2.4 on Software Implementation Technology (IFIP WG2.4). Essex, Vermont, USA. Oct, 2017.
[abstract] [slides.pdf] [slides.key] -
Abstracting Definitional Interpreters.
International Conference on Functional Programming (ICFP). Oxford, England. September, 2017.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.
International Conference on Functional Programming (ICFP). Nara, Japan. September, 2016.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video] -
Compositional and Mechanically Verified Program Analyzers.
ECOOP Doctoral Symposium (ECOOP-DS). Rome, Italy. July, 2016.
[pdf] [abstract] [slides.pdf] [slides.key] -
Constructive Galois Connections.
New Jersey Programming Languages and Systems Seminar (NJPLS). Philadelphia, Pennsylvania, USA. May, 2016.
[slides.pdf] [slides.key] -
Adventures in Abstract Interpretation.
Research Seminar. University of Utah. February, 2016.
[slides.pdf] [slides.key] [video] -
Constructive Galois Connections: With Applications to Abstracting Gradual Typing.
Research Seminar. University of Chile. January, 2016.
[slides.pdf] [slides.key] [demo.agda] -
Formally Verifying and Deriving Gradual Type Systems.
Class Presentation. University of Maryland CMSC 631. December, 2015.
[slides.pdf] [slides.key] -
Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis.
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA). Pittsburgh, Pennsylvania, USA. October, 2015.
[pdf] [abstract] [bibtex] [ACM] [arXiv] [slides.pdf] [slides.key] [video]
Professional Activities
- NSF Panels: 2 SHF; (dates confidential)
- Steering Committee: TyDe 2020, 2021 (chair), 2022
- Organizing Chair: TyDe 2019 (co); OOPSLA SRC 2019 (co); ECOOP DS 2017 (co)
- Program Committee (PC): PLDI 2021; TrustNLP 2021; ICFP 2020; TyDe 2018; IFL 2018
- External/Extended Review Committee (ERC): PLDI 2020; ICFP 2018
- Posters Committee: ICFP SRC 2019 (+ judge); ECOOP 2019 Posters
- Mentoring Workshops: PLMS 2018 (panel)
- Video (co-)Chair: OOPSLA 2017; POPL 2017; PLDI 2017, 2016; ECOOP 2017, 2016; ICFP 2013
- Artifact Evaluation Committee (AEC): POPL 2016
- Student Volunteer: POPL 2016, ICFP 2013 (chair)
- Logo Designer: ICFP 2013
Teaching
- UVM CS 225: Programming Languages / Spring 2020
- UVM CS 295A: Software Verification / Fall 2019
- UVM CS 225: Programming Languages / Spring 2019
- UVM CS 295A: Software Verification / Fall 2018
- UVM CS 225: Programming Languages / Spring 2018
Past Students
- Chike Abuah (PhD co-advised)
- Ryan Estes (PhD co-advised)
- Kristin Mills (MS co-advised)
- Tim Stevens (MS co-advised)
- Adam Barson (BS)
- Jacob Wunder (BS co-advised)
- Lindsey Stuntz (BS co-advised)
- Phillip Nguyen (BS co-advised)
- Ramy Koudsi (BS)
Short Bio
David is a Principal Scientist at Stealth Software Technologies where he builds programming languages and analysis tools that help programmers build reliable software. These tools are designed specifically for security-sensitive and privacy-sensitive settings, and result in systems that are immune to large classes of security and privacy defects. David received his BS from the University of Utah, MS from Harvard University, PhD from the University of Maryland, and was previously an Assistant Professor at the University of Vermont before joining Stealth Software Technologies.
Medium Bio
David is a Principal Scientist at Stealth Software Technologies where he builds programming languages and analysis tools that help programmers build reliable software. These tools are designed specifically for security-sensitive and privacy-sensitive settings, and result in systems that are immune to large classes of security and privacy defects. David approaches building better systems through a number of methods, including static and dynamic program analysis, type systems, mechanized verification, differential privacy and secure multiparty computation. David builds tools that secure systems against a wide range of adversaries, ranging from directly malicious actors, to the well-intended software developer who accidentally misused security-or-privacy-relevant technology, such as cryptography or differential privacy. To combat these adversaries, David co-designs programming languages in concert with verification tools while also maintaining a usable, high-level, and general-purpose programming environment for application developers. David received his BS from the University of Utah, MS from Harvard University, PhD from the University of Maryland, and was previously an Assistant Professor at the University of Vermont before joining Stealth Software Technologies