• Skip to primary navigation
  • Skip to main content
SRI logo
  • About
    • Press room
    • Our history
  • Expertise
    • Advanced imaging systems
    • Artificial intelligence
    • Biomedical R&D services
    • Biomedical sciences
    • Computer vision
    • Cyber & formal methods
    • Education and learning
    • Innovation strategy and policy
    • National security
    • Ocean & space
    • Quantum
    • Robotics, sensors & devices
    • Speech & natural language
    • Video test & measurement
  • Ventures
  • NSIC
  • Careers
  • Contact
  • 日本支社
Search
Close
Blog archive January 16, 2015

Why the Cyber Security Industry Should Be Smitten with Smten

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.

Share this

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you.

Expect a response within 48 hours.

Career call to action image

Make your own mark.

Search jobs

Our work

Case studies

Publications

Timeline of innovation

Areas of expertise

Institute

Leadership

Press room

Media inquiries

Compliance

Careers

Job listings

Contact

SRI Ventures

Our locations

Headquarters

333 Ravenswood Ave
Menlo Park, CA 94025 USA

+1 (650) 859-2000

Subscribe to our newsletter


日本支社
SRI International
  • Contact us
  • Privacy Policy
  • Cookies
  • DMCA
  • Copyright © 2023 SRI International
Manage Cookie Consent
To provide the best experiences, we use technologies like cookies to store and/or access device information. Consenting to these technologies will allow us to process data such as browsing behavior or unique IDs on this site. Not consenting or withdrawing consent, may adversely affect certain features and functions.
Functional Always active
The technical storage or access is strictly necessary for the legitimate purpose of enabling the use of a specific service explicitly requested by the subscriber or user, or for the sole purpose of carrying out the transmission of a communication over an electronic communications network.
Preferences
The technical storage or access is necessary for the legitimate purpose of storing preferences that are not requested by the subscriber or user.
Statistics
The technical storage or access that is used exclusively for statistical purposes. The technical storage or access that is used exclusively for anonymous statistical purposes. Without a subpoena, voluntary compliance on the part of your Internet Service Provider, or additional records from a third party, information stored or retrieved for this purpose alone cannot usually be used to identify you.
Marketing
The technical storage or access is required to create user profiles to send advertising, or to track the user on a website or across several websites for similar marketing purposes.
Manage options Manage services Manage vendors Read more about these purposes
View preferences
{title} {title} {title}