Kinan Dak Albabbabman@bu.edu
LinkedIn | Github | Extended CV | Resume
Department of Computer Science
111 Cummington St
Boston, MA, 02215
- I joined the NETMIT research group at MIT CSAIL as a visting student, where I am working on the Emerald project with Prof. Dina Katabi, I am working on backend systems for IoT home devices, cloud-based data analytics services, and stream processing.
- I am desiging and co-teaching a course in Spring 2019 on Dependently-Typed Automated Systems with Prof. Assaf Kfoury. The course will go over the theoretical foundations (up to the calculus of inductive constructions) and practical use of four systems (Coq, Lean, ATS, Agda), with examples from Operating and Distributed Systems, Certified Compilers, and Computer-assisted Cryptographic proofs. PhD Students from the Boston area are welcome to attend.
BiographyI am a PhD student in the Department of Computer Science at Boston University. I am co-advised by Prof. Assaf Kfoury and Prof. Azer Bestavros . I joined the PhD programing in September 2016.
My research lies in ensuring safety and security of cloud-based distributed systems, I am interested in desiging cryptographic protocols for distributed systems at scale to ensure security and privacy, and 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 worked mainly with Prof. Paul Attie and Prof Mohamad Jaber.
You can find my CV here.
ResearchI work on a variety of research projects, spanning areas from formal verification, systems design, and applied cryptography.
I am working with Prof. Dina Katabi in the Networks @ MIT research group on the Emrald project. I am working 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, ...).
I am interested in combining theorem proving and popular imperative languages (in particular Java), to achieve high levels of confidence in the correctness of code.
Industry WorkI worked as a senior software developer for a startup 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.
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).
- CMPS 272: Operating Systems (Fall 2015): Teaching assistant (American University of Beirut).
- CMPS 211: Discrete Structures (Spring 2016): Teaching assistant (American University of Beirut).
- CMPS 257: Theory of Computation (Fall 2014 and 2015): Peer tutoring (American University of Beirut).
- CS 332: Theory of Computation (Spring 2017): Teaching Fellow (Boston University).
- 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
InternshipsI intered as a software engineer fellow in the summers of 2017 and 2018 at Boston University Software & Application Innovation Lab (BU SAIL).
BU SAIL is a professional software design and development lab that serves as a collaborative resource for computational and data-driven research efforts across 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 also worked on designing efficient privacy-preserving protocols for geographical algorithms (mainly for route recommendation).
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
- 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 (Sep-3-2017)
AwardsHairir Institute for Computing (HIC @ BU) Gradute Student Fellow (2017-2018)
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.