Posts by Collection



Automated Attacker Synthesis for Distributed Protocols

Published in SAFECOMP, 2020

In this paper we take a formal approach to the automated synthesis of attackers, ie adversarial processes that can cause the protocol to malfunction. Specifically, given a formal threat model capturing the distributed protocol model and network topology, as well as the placement, goals, and interface (inputs and outputs) of potential attackers, we automatically synthesize an attacker.

Recommended citation: von Hippel, M., Vick, C., Tripakis, S., & Nita-Rotaru, C. (2020). Automated Attacker Synthesis for Distributed Protocols. arXiv preprint arXiv:2004.01220.

Counterexample Classification

Published in , 2021

In model checking, when a given model fails to satisfy the desired specification, a typical model checker provides a counterexample that illustrates how the violation occurs. In general, there exist many diverse counterexamples that exhibit distinct violating behaviors, which the user may wish to examine before deciding how to repair the model. Unfortunately, obtaining this information is challenging in existing model checkers since (1) the number of counterexamples may be too large to enumerate one by one, and (2) many of these counterexamples are re- dundant, in that they describe the same type of violating behavior. In this paper, we propose a technique called counterexample classification. The goal of classification is to partition the space of all counterexam- ples into a finite set of counterexample classes, each of which describes a distinct type of violating behavior for the given specification. These classes are then presented as a summary of possible violating behaviors in the system, freeing the user from manually having to inspect or an- alyze numerous counterexamples to extract the same information. We have implemented a prototype of our technique on top of an existing for- mal modeling and verification tool, the Alloy Analyzer, and evaluated the effectiveness of the technique on case studies involving the well-known Needham-Schroeder protocol with promising results.



Functional Programming Tutor

Course, Northeastern, CS2500, 2018

Position held for 2 semesters. Led weekly office hours for introductory functional programming course. Graded dozens of homework each week. Developed mastery of basic functional programming concepts. Course taught in Racket.

Peer Mentor

Course, Northeastern, 2019

Position held for 1 semester. Led weekly one hour course for job preparation for undergraduates.
Held one hour one-on-one interview preparation meetings with students 2 times a week throughout the semester.