This post describes a part of our work NodeMedic-FINE, an automated tool to find arbitrary command injection and arbitrary code execution vulnerabilities in Node.js packages. While I am the sole author of this blog post, the work it describes was done in collaboration with Darion…
Randomness is a fundamental component of numerous real-world protocols. It is used everywhere, from ensuring fairness in the green card lottery to its application in clinical trials, financial audits, and various blockchain technologies.
For these protocols, randomness must satis…
In 2006, Senator Ted Stevens infamously described the Internet as a “series of tubes’‘, where “filled tubes’’ delayed his email. While Senator Stevens was ridiculed at the time for his simplistic understanding of the Internet, his characterization was not entirely wrong:
“It’s …
It is nearly inevitable that bugs will appear in a codebase during software development. To catch these bugs before they lead to real-world consequences,
the formal verification community has developed a wide variety of tools for ensuring code correctness. These tools fall
into t…
Satisfiability Modulo Theories (SMT) solvers are powerful tools
that answer logical and mathematical questions.
As an example, let’s say I want to know whether there exists integers
\(a, b, c\) such that \(3a^{2} -2ab -b^2c = 7\).
To ask an SMT solver, I need to write an SMT quer…
\[
\gdef\lf{\left \lfloor}
\gdef\rf{\right \rfloor}
\]
Imagine using a popular messaging app that includes a contact discovery feature to find which of your phone contacts are already using the service and to get information on how to communicate with them. While convenient, this…
Truly Anonymous Service Providers can offer users confirmed privacy, but also allow inappropriate behavior 😳
Anonymous Blocklisting permits blocking ill-behaved users without denanonymizing them. Specifically, the service provider blocks individual posts, and the benign users u…
In large cloud service providers such as AWS, the customer provides an attributed graph and would like to perform tasks such as recommendations (i.e., link prediction in a graph) using message-passing methods within restricted budgets.
An attributed graph consists of both the gra…
Information retrieval is a pervasive aspect of our digital life, yet the process of retrieval consistently compromises the privacy of the users (i.e., the information requesters). For example, when you access a website, you need to first retrieve the website’s IP address from a D…
Data center networks are similar to large cities:
they are at massive scale, and there exist many available roads/paths between a pair of source and destination.
To move data from one place to another, we transfer data in chunks of bytes known as packets (roughly analogous to veh…
