Mining and Understanding Software Enclaves (MUSE)

As computing devices become more pervasive, the software systems that control them have become increasingly more complex and sophisticated. Consequently, despite the tremendous resources devoted to making software more robust and resilient, ensuring that programs are correct—especially at scale—remains a difficult and challenging endeavor. Unfortunately, uncaught errors triggered during program execution can lead to potentially crippling security violations, unexpected runtime failure or unintended behavior, all of which can have profound negative consequences on economic productivity, reliability of mission-critical systems, and correct operation of important and sensitive cyber infrastructure.

Vulnerabilities manifest when implementations do not conform to design. Determining program correctness thus fundamentally requires a precise understanding of a program’s intended behavior, and a means to convey this understanding unambiguously in a form suitable for automated inspection. Having useful, comprehensible and efficiently checkable program specifications is therefore critical for gaining high assurance and confidence of complex software systems. Often, however, the behaviors exposed by a program's implementation do not match those defined by the program's specification, in large part because the task of writing useful, correct and efficiently checkable specifications is often as hard as the task of writing the implementations that purport to satisfy it.

To help overcome these challenges, DARPA has created the Mining and Understanding Software Enclaves (MUSE) program. MUSE seeks to make significant advances in the way software is built, debugged, verified, maintained and understood. Central to its approach is the creation of a community infrastructure built around a large, diverse and evolving corpus of software drawn from the hundreds of billions of lines of open source code available today.

An integral part of the envisioned infrastructure would be a continuously operational specification mining engine. This engine would leverage deep program analyses and foundational ideas underlying big data analytics to populate and refine a database containing inferences about useful properties, behaviors and vulnerabilities of the program components in the corpus. The collective knowledge gleaned from this effort would facilitate new mechanisms for dramatically improving software reliability, and help develop radically different approaches for automatically constructing and repairing complex software.

Among the many envisioned benefits of the program are scalable automated mechanisms to identify and repair program errors, and specification-based tools to create and synthesize new, custom programs from existing corpus elements based on properties discovered from this mining activity.

The MUSE program is interested in close and continued collaboration of experts from a range of fields, including but not limited to: programming languages, program analysis, theorem proving and verification, testing, compilers, software engineering, machine learning, databases, statisticians, systems and a multitude of application domains. The program intends to emphasize creating and leveraging open source technology.

The Special Notice for Muse is available at http://go.usa.gov/BwgG. The Broad Agency Announcement (BAA) for MUSE is available at http://go.usa.gov/BuR5. To familiarize potential participants with the technical objectives of MUSE, DARPA has scheduled a Proposers' Day on Friday, March 7, 2014, at DARPA’s offices in Arlington, Va. For details, visit www.sa-meetings.com/MUSE. Registration closes on Friday, February 28, 2014, at 5 p.m. ET. For more information, please email MUSE@darpa.mil.

컴퓨팅 디바이스가 점점 많아지고 그를 통제하는 소프트웨어 시스템 또한 점점 복잡하고 정교해지고 있다. 또 소프트웨어를 튼튼하게 만드려는 수많은 노력에도 불구하고 옳다고 확신할 수 있는 프로그램을 만드는 것은 매우 어려운 과제로 남아있다. 불행히도 미리 찾지 못했던 에러가 실행중에 발생해서 보안에 심각한 위협이나 의도치 않았던 현상을 발생시킬 수도 있으며, 이는 경제적으로도, 사이버 인프라에도 심각한 영향을 미친다.

취약점은 구현이 디자인과 맞지 않을 때 발생한다. 프로그램의 정확도를 결정하기 위해서는 프로그램의 원래 의도와 이 의도가 어떻게 이뤄졌는지에 대한 확실한 이해가 필요하다. 즉, 구체적이고 효율적이며 checkable한 사전 시방서(specification)가 소프트웨어 시스템의 보증을 위해 반드시 필요하다. 하지만 이러한 시방서를 만드는 것 자체가 기술된대로 구현하는 것만큼 어렵기 때문에 프로그램의 구현이 원래의 디자인과 맞지 않는 것은 흔한 일이다.

이러한 문제를 해결하기 위해 DARPA는 Mining and Understanding Software Enclaves (MUSE) 프로그램을 만들고 있다. MUSE는 소프트웨어가 설계, 디버그, 증명, 유지, 그리고 이해되는 모든 과정을 발전시키려 한다. 이 프로그램의 가장 핵심사항은 최근의 오픈소스코드의 수백억의 긴 코드라인을 이용해서 만든 다양한 소프트웨어의 corpus에 대해 커뮤니티 인프라 구조를 구축하는 것이다.

인프라구조에서 중요한 것은 지속적인 운영상의 specification 마이닝 엔진이다. 이 엔진은 corpus 속 프로그램의 주요 특성, 행위, 취약점 등이 담긴 데이터베이스를 이용한 빅데이터 분석에 사용될 수 있는 프로그램 분석, 기초적인 아이디어를 제공한다. 이렇게 모인 수집 정보들은 소프트웨어의 신뢰성을 개선시킬 새로운 메커니즘을 가능하게 하고, 복잡한 소프트웨어를 자동적으로 설계하고 정비하는 새로운 방법론을 제시한다.

이 프로그램의 많은 이점 중 하나는 프로그램의 오류를 식별하고 정비하는 자동화된 매커니즘과, 마이닝을 통해 발견된 기존 corpus 요소에서 새로운 커스텀 프로그램을 만들 수 있는 specification 기반 도구들이다.

MUSE 프로그램은 제한을 두지 않고 여러 분야의 전문과들과 함께 지속적인 연구를 하는 것에 관심을 두고 있다(programming languages, program analysis, theorem proving and verification, testing, compilers, software engineering, machine learning, databases, statisticians, systems and a multitude of application domains). 이 프로그램은 오픈소스기술을 창안하고 활용하는데에 중점을 둔다.