Semantic security bugs resulting from logic flaws severely undermine the security of critical software systems. For example, attackers exploited a recent semantic security bug (CVE-2017-5638) in Apache Struts to steal sensitive personal data of 143 million customers of Equifax. Despite the severity of such semantic security bugs, there is no generic method for detecting these bugs. The key challenge is that semantic bugs, unlike memory corruption bugs, do not have any program-independent side-effects like crashing. Therefore, semantic security bugs are hard to detect without formal specifications of the program under test. Unfortunately, full formal specifications (test oracles) are usually not available even for security critical software as these specifications are difficult to create and keep in sync with functionality changes.

Our longer-term goal is to develop SESPO, a generic framework for automatically detecting semantic security bugs using pseudo-oracle testing—a way to create test oracles by comparing behaviors of related executions even when complete specifications are not available. SESPO will use two main classes of pseudo-oracles: (i) Differential Testing to compare outputs of different independent programs with similar functionality and (ii) Metamorphic Testing to check the relationship between outputs from multiple executions of the same program with different inputs.

We are currently looking for one or more undergraduate/MS project students to perform a relatively short-term project for academic credit: devising metamorphic relations corresponding to some security properties of Java and/or C/C++ software.  A “metamorphic relation” specifies a relationship between input/output pairs.  In particular, if you have a given input i and its already known output o (already known because you ran the software with input i), the relation defines 1. a constructor, 2. a predictor and 3. a checker, where the constructor crafts a new input i’ from i, the predictor determines what the output o’ ought to be from the already known i, o and i’, and the checker compares the real output o” (when you run the software with input i’) to the predicted output o’.  If o” is not consistent with o’, we know there’s a bug in the software (the checker is often but not necessarily equality).  For example, if you ran a sort program on a list of elements as input to produce sorted output, permuting the original input list to derive the new input should result in the identical output except for “ties”.

We will train you in the concepts of metamorphic testing.  Your job will be to find a reasonable number of different metamorphic relations relevant to security properties of real-world software, where inputs come from untrusted users.

To learn more, please contact Prof. Kaiser, kaiser@cs.columbia.edu.