Kinan Dak Albabbabman@bu.edu
LinkedIn | Github | Resume
Department of Computer Science
111 Cummington St
Boston, MA, 02215
BiographyI am a PhD student in the Department of Computer Science at Boston University. I was advised by Prof. Andrei Lapets. I work closely with Professors Prof. Assaf Kfoury, Mayank Varia and Prof. Azer Bestavros . I joined the PhD programing in September 2016. I am currently interning at Google working with Dr. Konstantin Weitz and Dr. Stefan Heule on formal verification and testing of network switches.
My research lies in building and reasoning about computer systems and programs. I have been working on desiging cryptographic protocols for distributed systems at scale to ensure security and privacy. I am interested in utilizing formal program analysis techniques (proof assistants) and novel programming models and frameworks to reason about the correctness and security of whole system at large.
I recieved a B.S. in Computer Science in 2015 from the American University of Beirut with a Minor in Mathematics. I mainly worked with Prof. Paul Attie and Prof Mohamad Jaber.
You can find my Resume here.
ResearchI work on a variety of research projects, spanning areas from systems design, applied cryptography, and formal verification.
I am working on verifying concrete implementations of the snapping mechansim in the Coq theorem prover. The verification combines probabilistic coupling based relational reasoning with reasoning about floating point arithmetic and errors. Joint work with Jiawen Liu and Marco Gaboardi.
I am running an informal reading group on verifying operating systems kernels and hypervisors, with a particular focus on security and temporal isolation. I am also co-organizing the programming language reading group for Fall 2019 at Boston University with Will Blair.
I was a visting student at MIT CSAIL with Prof. Dina Katabi in the Networks @ MIT research group on the Emrald project. I worked on desiging, implementing, and deploying various systems running on IoT devices and on the cloud, for sensing, streaming, collecting, and analysing data at scale.
I worked with Prof. Paul Attie on Subtractive Model Repair. Given a model (a Kripke Structure) of a sequential or concurrent program and specifications (CTL Formula), we attempt to repair the structure by removing states and transitions. We use the model and specifications to construct a SAT formula that is satisfiable if and only if the model is repairable, we use the resulting satisfying assignemnt to deduce which states and transitions are removed from the structure. We use a pair-wise representation of the model to avoid state explosion as the number of processes grow. We developed a tool Eshmun that can be used for repairing Kripke Structures, as well as a variety of other features (Model Checking, Abstractions, ...).
Industry WorkGoogle: I am interning at Google during the summer of 2020. I am working with the core infrastructure team on formal verification and testing of network switches, by analyzing SDN programs and generating test packets that cover path combinations in the data and control plane, using SMT solving.
Software Application & Innovation Lab: I was a software engineering fellow at the Software & Application Innovation Lab (SAIL), a professional research software engineering lab within Boston University. I worked on developing a back-end platform that supports performing MPC on-the-fly between clients using different devices including mobile and web applications. I have led and produced several open source frameworks for secure computation, and worked with and mentored several interns at SAIL from high-schoolers to graduate students.
Interactive Life: I worked as a senior software developer for Interactive Life from August 2015 to August 2016. Interactive Life is a startup based in Seattle, WA. It provides apps and services for businesses and organizations to help them engage and reach to a wide range of users. The company provided solutions for a wide range of sectors including health-care (clinics), interactive TV, churches, and media agencies. Some of my responsibilites included:
- Android Mobile Development: I participated in developing an Android SDK that provides a large API for common functionalities between the different apps, I worked extensively on the design of the SDK and its interactions with the apps. I also worked on some of the apps implementations and UI.
- Backend Development: I was responsible for developing and maintaining a specialized backend server that delievers and trigger data to the mobile apps through RESTful APIs. The backend provided authentication and profile management for the end-users as well.
- Architecture: I also worked on the overall architecture of the platform, including designing the different backend servers and their roles, the SDK and libraries for both Android and iOS, and choosing technologies for different components.
Fetch: During my undergraduate studies, I worked as an intern for Fetch in the summer of 2014. I worked on a web application that is used by companies and service providers to analyse their clients comments on social media. The web application would gather data from social media, and use sentiment analysis to produce reports that include the overall satisfaction and amount of engagment of clients. I have worked as a freelancer in 2014-2015 on different projects, mostly small and medium sized websites and web applications, as well as one desktop application (java-based).
CS 591 L1 (Fall 2019): Embedded Languages
Instructor of Record. I am designing and teaching the course following the departure of Prof. Andrei Lapets.
CS 591 K1 (Spring 2019):
Foundations and Pragmatics of Dependently-Typed Automated Systems.
I was the co-designer and co-instructor of the course with Prof. Assaf Kfoury. Going over the theoretical foundations (up to the calculus of inductive constructions) and practical use of four systems (Coq, Lean, ATS, Agda).
Summer Challenge (Summer 2017, Summer 2018).
I taught and designed the entire course on Computer Science in BU's Summer Challenge Program: an extensive 2 weeks program for rising high school students. Course Website
CS 332: Theory of Computation (Spring 2017).
Teaching Fellow with Prof. Steve Homer.
American University of Beirut:
Tutorial: Deploying Secure Multi-Party Computation on the Web Using JIFF
Kinan Dak Albab, Rawane Issa, Andrei Lapets, Peter Flockhart, Lucy Qin, Ira Globus-Harris
2019 IEEE Cybersecurity Development (SecDev) 2019
Role-Based Ecosystem for the Design, Development, and
Deployment of Secure Multi-Party Data Analytics Applications
Andrei Lapets, Kinan Dak Albab, Rawane Issa, Lucy Qin, Mayank Varia, Azer Bestavros, Frederick Jansen
2019 IEEE Cybersecurity Development (SecDev) 2019
From Usability to Secure Computing and Back Again
Lucy Qin, Andrei Lapets, Frederick Jansen, Peter Flockhart, Kinan Dak Albab, Ira Globus-Harris, Shannon Roberts, Mayank Varia
2019 Symposium on Usable Privacy and Security (USENIX SOUPS)
Accessible Privacy-Preserving Web-Based Data Analysis for Assessing and Addressing Economic Inequalities
Andrei Lapets, Frederick Jansen, Kinan Dak Albab, Rawane Issa, Lucy Qin, Mayank Varia, Azer Bestavros
Proceedings of the 1st ACM SIGCAS Conference on Computing and Sustainable Societies (ACM COMPASS)
San Jose, CA, USA, 2018, Article 48
Brief Announcement: Federated Code Auditing and Delivery for MPC
Frederick Jansen, Kinan Dak Albab, Andrei Lapets, Mayank Varia
Stabilization, Safety, and Security of Distributed Systems. SSS 2017
Lecture Notes in Computer Science, vol 10616. Springer, Cham
Scalable Secure Multi-Party Network Vulnerability Analysis via Symbolic Optimization
Kinan Dak Al Bab, Rawane Issa, Andrei Lapets, Azer Bestavros, and Nikolaj Volgushev
2017 IEEE Security and Privacy Workshops (SPW)
San Jose, CA, USA, 2017, pp. 211-216
Model and Program Repair via SAT Solving
Paul C. Attie, Kinan Dak Al Bab, and Mohamad Sakr
ACM Transactions on Embedded Computing Systems (TECS)
Volume 17 Issue 2. December 2017
A High-level Modeling Language for the Efficient Design, Implementation, and Testing of Android Applications
Mohamad Jaber, Ylies Falcone, Kinan Dak-Al-Bab, John Abou-Jaoudeh and Mostafa El-Katerji
STTT: International Journal on Software Tools for Technology Transfer
Volume 20 Issue 1. November 2016
Model and Program Repair via SAT Solving
Paul C. Attie, Ali Cherri, Kinan Dak Al Bab, Mohamad Sakr, and Jad Saklawi
MEMOCODE'15: 13th ACM-IEEE International Conference on Formal Methods and Models for System Design
Austin, Texas, USA. September 2015
- Carousels: automatic resource estimation for obliv rust and JIFF programs (Code, Prototype).
- OPRF: TypeScript and WebAssembly implementation of a two-party oblivious pseudorandom function from DDH on elliptic curves (Code, npm).
WebMPC: A framework for conducting statistical analysis and surveys under MPC in the web (Code).
Several versions of this framwork were deployed throughout 2016-2020 for conducting data analytics by the Boston Women Workforce Concil as well as the Boston Chamber of Commerce.
- Eshmun: Automatic Model Repair (Binaries and Blog).
- JIFF: a practical and configurable MPC framework for the web. Brown System Seminar, Hosted by Prof. Malte Schwarzkopf. (December-6-2019)
- Implementing Secure Multi-Party Computation: Invited talk at the Red Hat Summit. Slides (May-6-2019).
- Scalable Secure Multi-Party Network Vulnerability Analysis via Symbolic Optimization: Paper Presentation at WTMC 2017. PDF (May-25-2017).
- Managing Trust in the Cloud (with Rawane Issa): Invited talk at the American University of Beirut (AUB) first North American Computer Science Alumni Reunion. PDF (September-3-2017).
AwardsTeaching Excellence Award: Boston University, Department of Computer Science, 2020. Vivli and Microsoft datatheon on Privacy and Utility of Rare Diseases Datasets: Award for Outstanding Graduate Submission, June 2019.
Hariri Institute for Computing (HIC @ BU) Gradute Student Fellow 2017-2020.
Mark Sawaya Excellence Award , Best Graduating Student in Computer Science (AUB), 2015.
AUB Dean's Honor List: Fall 2013, Spring 2014.
1st Place in ACM - Lebanese Collegiate Programming Contest (Team Khawarizmi), 2015.
1st Place in AUB's Supernacci Math Programming Competition (Team 0xdeadbeef), 2015.