- Technical Skills
University of Minnesota (Ph. D.)
|Degree||Doctor of Philosophy in Computer Science (in progress)|
|Advisor||Dr. Gopalan Nadathur|
|Thesis||Reasoning about Linear Logic Specifications (working title)|
|Time Frame||2011 — 2017|
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|
|Time Frame||2013 — present|
Formal Software Verification (2015-present)
AutoCorress is an extension to the Isabelle Theorem Prover that encodes a large subset of the C programming language into a monadic form better suited for human reasoning, i.e., it closely resembles the original code. My task is to understand how to effectively use AutoCorress to verify relevant properties relating to Rockwell Collins work on the SMACCMS project.
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.
|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 experiment 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.
University of Minnesota
|Time Frame||2011 — 2015|
Advanced Programming Principles 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.
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’s 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.
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 Resilent Computing Security (ARCS), November 3rd and 4th 2004, Sante Fe, New Mexico.
|Programming Languages||OCaml, Python, C, Java, Teyjus, C++, Perl, Haskell|
|Verification Tools||Isabelle, AutoCorres, Abella, jkind, Coq|
|General Development Tools||Emacs, GDB, Valgrind, Eclipse, Vim, Xtext, SQLite|
|Web Development Tools||Pyramid, Jekyll, Ziggurat Foundations|