Applying novel program analysis and artificial intelligence to advance the state-of-the-art in computer security.

Mission

Aarno Labs is an R&D firm that specializes in solving extremely difficult computer security challenges by developing advanced automated techniques. Our researchers offer pioneering and deep expertise across multiple fields of computer science. Aarno Labs seeks short and long-term R&D contracts from organizations with high security requirements looking for aggressive solutions to their computer security challenges.

Team

Aarno labs is staffed by researchers with significant academic and industry experience in computer security and program analysis research. Combined, our principal researchers have led over a dozen research grants from DoD and intelligence agencies, and published over 75 research papers in the fields of program analysis and security.

Technologies

Aarno labs has extensive expertise in applying static and dynamic program analysis to find and patch program vulnerabilities and to uncover malicious behaviors. More specifically, we have deep expertise in mobile malware analysis, automatic bug finding, automatic program repair, precise whole-program static analysis, low-overhead dynamic code instrumentation, program verification, and machine learning.

Principal Researchers

Dr. Stelios Sidiroglou-Douskos

Dr. Stelios Sidiroglou-Douskos

Dr. Sidiroglou-Douskos is an expert in the areas of systems, computer security and programming languages. Prior to founding Aarno Labs, Stelios was a research scientist at MIT CSAIL. At MIT, stelios was the lead researcher on DARPA’s MRC and MUSE programs and served as the lead developer in DARPA’s application communities project. Stelios has published over 50 research papers in the top programming languages and computer security conferences. He was also the co-founder of Locu, Inc which was acquired by Godaddy.

Jeff Perkins

Jeff Perkins

Mr. Perkins is an expert in automatic program repair, dynamic invariant detection, automatic test generation, type inference, and dynamic instrumentation. Prior to Aarno Labs, Jeff was a full-time research scientist at MIT CSAIL. At MIT, he was the program manager and lead researcher for DARPA's Application Communities program and IARPA's STONESOUP program. He has over 20 years of experience in the design, development, and management of software and systems. Jeff has published dozens of works in major research conferences.

Dr. Michael Gordon

Dr. Michael Gordon

Dr. Gordon is an expert in static and dynamic program analysis, malware analysis, and mobile application security. Before Aarno Labs, Michael held a research position at MIT, publishing in top research conferences. As MIT's lead investigator on DARPA’s APAC program, Michael led the development of best-in-class global static analyses for exposing malware in mobile apps, achieving unsurpassed malware diagnosis accuracy in the last six APAC engagements. The technology is currently being transitioned to the DoD. Michael earned his MS and PhD from MIT in computer science.

Projects

A sample of Aarno Labs' public projects and grants.

DroidSafe

The DroidSafe project develops effective program analysis techniques and tools to uncover malicious code in Android mobile applications. The core of the system is a static information flow analysis that reports the context under which sensitive information is used. For example, "Application A has the potential to send location information to network address 128.6.21.6 on 'Button B’ press". The DroidSafe project invested significant time developing a comprehensive semantic model of Android runtime behaviors alongside the analysis to achieve acceptable precision, accuracy, and scalability for real-world Android applications. The combined system has been demonstrated to be the most precise and accurate information flow analysis for Android applications. The analysis results can be used to automatically check applications for security policy violations, and the results can help a human analyst inspect sensitive behaviors of an app, increasing accuracy and throughput of application vetting. For each of the last six DARPA APAC engagements to date, the DroidSafe team has been unsurpassed in malware diagnosis accuracy with the least amount of human analysis time.

Principal Investigator: Dr. Michael Gordon

Partners: MIT and Kestrel Institute

Funding Source: DARPA APAC Program

Dark Corners

Sound static program analysis promises exhaustive detection of many classes of program errors and, ideally, verification that the program is free of these errors. However, the critical issue is the lack of precision that such analyses inevitably encounter when analyzing the programs that occur in practice. Our hypothesis is that, in existing programs, only a small percentage of the code is responsible for the lack of precision for verification tasks. Aarno Labs is developing program analysis tools that identify and mitigate the sources of imprecision in large, real-world programs. We are developing analysis technologies such that identify the exact source of imprecision in the implementation using techniques such as logical abduction. Furthermore, we are developing techniques to increase precision once target code is identified such as (1) Applying more expensive analysis techniques to this code; (2) Making manual changes to the code and/or adding annotations/dynamic checks to reduce the complexity; (3) Replacing the code with similar code from other implementations automatically; (4) Providing an alternative implementation that is easier to analyze but can be shown to match the existing implementation (with respect to memory safety).

Principal Investigator: Jeff Perkins

Partners: Professor Thomas Dillig

Funding Source: DARPA APAC Program

Targeted Automatic Patching

Overflow errors are an insidious source of software failures and security vulnerabilities. The accepted wisdom is to use a multitude of tools, such as involved software development strategies, dynamic bug finders and static analysis tools in an attempt to eliminate as many bugs as possible. However, experience has shown that it is very hard to achieve bug-free software. As a result, even under the best of circumstances, buggy software is deployed and developers face a constant and time-consuming battle of creating and releasing patches fast enough to fix newly discovered bugs. Patches can take days if not weeks to create, and it is not uncommon for systems to continue running unpatched applications long after an exploit of a bug has become well-known. As the scale of software deployments and the frequency of bug reports increase, it is clear that patch generation needs to be automated.

We are developing an automatic system (Targeted Automatic Patching or TAP) for finding and eliminating overflow errors. This system leverages bug finding tools to automatically generate inputs that expose overflow errors. TAP then uses a template-based synthesis approach to automatically generate software patches (both source and binary patches may be feasible). Template-based synthesis applies known error fixing patterns (or templates) in combination with formal methods, such as SMT solvers, to generate code that eliminates overflow errors. The proposed synergistic coupling of bug finding tools and automatic repair enables an unprecedented level of verifiable automation to automatically eliminate overflow errors

Principal Investigator: Dr. Stelios Sidiroglou-Douskos

Funding Source: DARPA MRC Program

Tunable Cyber Defensive Security Mechanisms

Evaluating security mechanisms is a difficult and manual process. To effectively compare different techniques, security analysts use synthetic bench- marks that are typically comprised of simple test cases or a combination of known vulnerabilities in an attempt to provide coverage for different classes of attacks. As such, security mechanisms adapt their techniques to guarantee good coverage for the synthetic benchmarks but provide little guarantees of their efficacy beyond that. To ensure accurate evaluation and comparison of competing security techniques on real-world programs, we need automated techniques for injecting realistic and verifiable vulnerabilities.

We developing a new technique and system for automatically generating and injecting realistic vulnerabilities to real-world applications. Our system uses targeted symbolic execution to discover program paths that could be used to generate vulnerabilities (e.g., integer overflows). The programs paths (i.e, symbolic constraints) are then modified using information from formal methods (e.g.,, using SMT solvers) to generate and inject new code , at the source- or binary-level, that is provably vulnerable (e.g., the system can prove that the generated conditions along a specific program path can lead to an integer overflow). The code is then obfuscated, using previously learned bug patterns, to look like native vulnerable code.

Principal Investigator: Dr. Stelios Sidiroglou-Douskos

Funding Source: DARPA SBIR Program

Careers

Aarno Labs is seeking talented and motivated individuals to improve software security and reliability. Applicants with experience in program analysis and software security are strongly encouraged to apply. To start the conversation, please email us at info@aarno-labs.com.