Dan DaCosta

chaosape@chaosape.com

• Professional
  • Amazon Web Services
  • Rockwell Collins
  • Lockheed Martin
• Education
  • University of Minnesota (Ph. D.)
  • Drexel University (M.S.C.S.)
  • Drexel University (B.S.C.S.)
• Teaching
  • University of Minnesota
• Publications
• Presentations
• Technical Skills

Professional

Amazon Web Services

VPC Reachability Analyzer / Inspector (2019-Present)

Significant contributor in internal AWS service relied on by VPC Reachability Analyzer and Inspector that applies formal methods to network configurations to answer questions about reachability between network resources.

Rockwell Collins

Secured Mathematically-Assured Composition of Control Modules[SMACCM] (2015-Present)

The SMACCM project developed provably secure tools for building UAV software. One of the platforms the SMACCM project targeted relied on the seL4 microkernel. On this platform, UAV software with different functional behavior was implemented as separate seL4 components. This provided each component a formally proved memory isolation invariant. Building a complete UAV system on this platform required a specification for how components were organized and communicated. The Trusted Build tool, something I helped develop, could translate these specifications to seL4’s less intuitive CAmkES build specification. Inter-Component communication could, however, allow one component to cause deadlock in one another. I solved this problem by modifying the Trusted Build tool to inject “monitors”, i.e., seL4 components for communication queue management, between two components susceptible to such deadlock. Correct behavior of these monitors was formally proved using AutoCorress.

The SMACCM project has ended and I am now working toward transfering the formal methods methodologies developed during the SMACCM project to other domains. Supervisory Control and Data Acquisition[SCADA] systems is one domain I am currently investigating for such transfer. This work can positively impact the safety of SCADA systems used to control critical infrastructure, e.g., electrical power grid systems, nuclear power station control systems, naval vessel control systems.

Air Force Research Lab’s (AFRL) Summer of Innovation (2017-2018)

Modeled after the “Google Summer of Code” program, the goal was to bring current formal methods theory and practice to bear on AFRL’s Unmanned Systems Autonomy Services software(UxAS). One critical component of UxAS provides waypoint sequences to proprietary autopilot software as the unmanned vehicle proceeds through a mission. I was responsible for porting this component to the seL4 microkernel. Furthermore, I verified a number of important properties about this component using AutoCorress; an extension to the Isabelle Theorem Prover that permits formal reasoning about C programs. This work contributed to a simulation where an unmanned vehicle remained on mission despite losing significant software functionality due to cyber attack. The results of our work were presented at S5. Our success during the Summer of Innovation influenced AFRL to fund our project past the original period of performance.

Automated System Requirement Verification (2013-2015)

Primary developer of SpeAR, a tool for system requirement specification and verification. SpeAR accepts formalized requirements and translated these requirements to a synchronous dataflow language. Another tool, jkind, translated this synchronous dataflow language to specifications suitable for SMT solvers. Through this series of translation, some properties of the specified system requirements could be verified in an automated fashion. SpeAR is written in Java using the Eclipse IDE with the xtext plugin.

Lockheed Martin

Malware Provenance (2010-2011)

Applied statistical modeling techniques to data retrieved via analysis of binary malware in an attempt to recover authorship information.

Transparent Protocol Layer Altering Network Device (2005-2010)

Worked with team members in the Advanced Technology Laboratory to design and implement a network device that could alter standard protocol behaviors to better suit network characteristics. The modifications to protocol behavior were implemented such that clients required no modification or non-standard configuration. The system allowed for easy modification of protocol behavior through configuration files and served as an experimental platform for new protocol modifications. The device was tested during a number of live aerial exercises. Later revisions of this project relied extensively on the Click Modular Router.

Buffer Overflow Mitigation (2003-2004)

Developed an experimental technique and framework that allowed buffer overflows to be detected and mitigated in c code at runtime. The prototype framework for this technique used the C Intermediate Language to transform programs into ones that would dynamically increase buffer size upon detection of overruns. Buffer overruns were detected using electric fence.

Education

University of Minnesota (Ph. D.)

Drexel University (M.S.C.S.)

Drexel University (B.S.C.S.)

Teaching

University of Minnesota

Advanced Programming Principles (x3)

Students were introduced to techniques for creating correct, robust, modular programs including: computing with symbolic data, recursion/induction, functional programming, impact of evaluation strategies, organizing data/computations around types, search-based programming, informal reasoning about programs.

Program Design and Development (x3)

A project based course intended to expose students to: principles of programming design/analysis, concepts in software development, large development using C/C++, data structures, debugging, files, I/O, state machines, testing, and coding standards.

Programming Languages (x2)

This course had two primary goals: (1) to expose students to language design principles, concepts, constructs; (2) to make students more familiar with language paradigms and their applications.

Publications

• Sam Bayless, John Backes, Dan DaCosta, Benjamin F. Jones, Nate Launchbury, Patrick Trentin, Kelsey Jewell, Sagar Joshi, Michael Q. Zeng, Nandita Mathews. Debugging network reachability with blocked paths. CAV 2021.

• Dan DaCosta. Towards Reasoning About Properties of Imperative Programs using Linear Logic. Report submitted in partial fulfillment of my written preliminaries.

• Dan DaCosta. pcapstitch: A tool to collect singleton one-way delay and loss measurements. Master thesis submitted in partial fulfillment of my Ms. of Computer Science from Drexel University.

• Dan DaCosta, Christopher Dahn, Spiros Mancoridis and Vassilis Prevalakis. Characterizing the Security Vulnerability Likelihood of Software Functions. In the IEEE Proceedings of the 2003 International Conference on Software Maintenance (ICSM’03), Amsterdam, The Netherlands, September, 2003.

Presentations

• Dan DaCosta. Formally Verifying Security and Compliance Mandates using AWS Network Access Analyzer. High Confidence Software and Systems Conference Series, May 8-10, 2023.

• Dan DaCosta and Gopalan Nadathur. Towards Reasoning about Properties of Imperative Programs using Linear Logic. Midwest Verification Days 2014, Columbia, MO, October 3-4, 2014.

• Jesse Brown and Daniel DaCosta. Synthesizing Adaptive Protocols by Selective Enumeration (SYNAPSE). Symposium on Click Modular Router, Belgium, November 23-24, 2009.

• Dan DaCosta and Todd Hughes. Adaptive Code Injection Attack Mitigation. Sante Fe Institute Business Network Topical Meeting - Adaptive and Resilient Computing Security (ARCS), November 3rd and 4th 2004, Sante Fe, New Mexico.

Technical Skills