Keeping pace with today’s evolving cyber threats is challenged not only by hackers’ sophistication, but also by the mind-boggling volume of attacks. The ramifications to individual privacy and global economies alone make cyber experts’ heads spin. How can we keep watch over massively increasing lines of software code being generated for millions of devices and services as automated coding and hacking increase the speed of the onslaught?
This question was the prevailing theme at the recent THREADS Conference at the New York University Polytechnic School of Engineering . The event assembled leading researchers and information security professionals tackling the new challenge of automating security in innovative ways. I delivered a presentation, “Smten and the Art of Satisfiability-based Search,” that examined approaches to cyber security challenges as they relate to the enormous coding manpower required to uncover pattern anomalies inherent to cyber threats.
First, let’s define satisfiability-modulo-theories (SMT) and the current landscape of SMT tools.
Satisfiability is essentially the problem of determining if a formula expressing a constraint has a model or solution. SMT, for its part, is the assembly language of search, utilized for pattern matching to solve challenging problems such as automatic test generation, model checking, and program synthesis. In principle, SMT enables software developers to quickly build high-performance solutions for specific applications based on a highly engineered computational solver. It avoids re-implementing the plethora of common algorithmic and low-level optimizations needed for performance.
For example, if I’m looking for something that matches a particular pattern and understand what the possibilities are, SMT can find the pattern match. The problem, until now, is that there hasn’t been a more clever solution than using SMT to check each possible option and execute a pattern match check. This is an inefficient, labor intensive and not very intelligent process.
The challenge with current SMT tools is the often-extensive translation time for the process. The programmer must write a translation from the special problem down to the level of an SMT query, pass the query to the SMT solver, get the answer, and translate it back up to the original domain. Though it is often straightforward to construct such a translation, ensuring that the translation and surrounding orchestration logic are implemented efficiently can take several months even for conceptually simple decision problems. Far too often, the orchestration of queries may dominate the computational and development costs.
So while there are many formal SMT tools on the market, they only work well if the user understands all of the computation underlying the query. In my talk at THREADS, I demonstrated that Smten-based applications require magnitudes less code and developer effort to achieve results comparable to standard SMT-based tools.
Like other coders, I was frustrated using traditional SMT solvers as verification tools in real applications. So I undertook Smten as a long-term side project.
What is Smten?
Smten is a Haskell-like (that is, standardized, general-purpose) programming language for orchestrating search queries. It automates the majority of orchestration-level work, leaving designers with only the high-level decomposition of their task into SMT-like queries. Smten effectively hides all of the details of efficient translation and interaction with SMT solvers and allows the programmer to directly represent the essence of their problem in a natural way. The tool performs the crucial but complex transformation for efficiency.
As shown in my THREADS presentation, Smten was rewritten to dramatically reduce the entry barrier for verification — it is usable by most engineers. By using modern programming languages to write SMT tools and by taking expensive SMT searches out of the exclusive domain of Ph.D.-level engineers, even a first-year undergrad could make a reasonable SMT tool.
For cyber security applications, Smten can be a game changer for its speed, performance, flexibility, and simplicity. Instead of spending months or even years to build a framework to ask just a single SMT question, Smten makes the process modular and re-usable for purposes beyond the initial program intent. This dramatically reduces time and labor requirements for SMT technology and, critically, democratizes access.
Leading SRI’s efforts in this area is very exciting. I believe Smten can become a key component in combatting cyber threats.
