Me :^)

Dan DaCosta

chaosape@chaosape.com


Professional


Amazon Web Services

Title Applied Scientist
Time Frame 2019 — Present

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

Title Ph.D. Intern
Time Frame 2013 — 2019

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

Title Senior Member of the Engineering Staff
Time Frame 2003 — 2011

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.)

Degree Computer Science Ph.D. Candidate [Not Completed]
Time Frame 2011 — 2019

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

Degree Master of Science in Computer Science
Advisor Dr. Spiros Mancoridis
Thesis pcapstich: A Tool to Collect Singleton One-way Delay and Loss Measurements
Time Frame 2002 — 2011

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

Degree Bachelor of Science in Computer Science
Time Frame 1998 — 2002

Teaching


University of Minnesota

Title Teaching Assistant
Time Frame 2011 — 2015

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



Presentations



Technical Skills


Programming Languages OCaml, Python, C, Java, Prolog, C++
Verification Tools Isabelle, AutoCorres, Abella, jkind, Coq
General Development Tools Emacs, GDB, Valgrind, Eclipse, Vim, Xtext, SQLite