Questions and Answers

What does the name Naccio mean?

Naccio is extracted from catenaccio, a style of soccer defense popularized by Inter Milan in the 1960s. Catenaccio sought to protect the Inter net from attacks, by wrapping potential threats with a marker and agressively removing potentially dangerous parts (that is, the ball) from attackers as soon as they cross the domain protection boundary (also know as the midfield line).

Naccio is also an acronym for Never Again Could Code Inflict Outrage, and No Acronym Can Cause Instant Ovations, but you'll need to by me a few beers before I am willing to admit it in public.

The correct pronouncation of Naccio is nah-CHEE-oh.

According to the Kabalarians, "Naccio" is a good choice for a baby name for a dramatist, musician, writer or artist.

What's the difference between Naccio and...

... Software Fault Isolation?

Software Fault Isolation is a technique for modifying object files to provide low-level code safety - that is, memory safety and jump safety. Software Fault Isolation is generally done to implement a fixed safety policy, such as disallowing writes outside the data segment. Naccio generalizes Software Fault Isolation to enable arbitrary, high-level safety policies to be expressed and enforced by modifying object files.

... Proof-Carrying Code?

Proof-Carrying Code is a mechanism where the execution environment statically verifies desired properties of a program before allowing it to execute. The program producer may include extra information in the object file that makes it easier to prove the desired properties (although the execution environment cannot trust this extra information).

Naccio starts from the assumption that it is almost always easier to modify an arbitrary program into one having a desired property, than to prove that property holds for an arbitrary program. Proof-Carrying Code is effective in enforcing simple properties such as memory safety, and has the advantage that once a property is verified the code can be run safely without any run-time overhead. In theory, it can be used to enforce general properties too, however, it is limited by automatic theorem proving technology, and it is unlikely that it will be able to enforce interesting high-level safety properties in the forseeable future.

... Java Sandboxing?

The Java Sandbox provides high-level security by allowing access to system resources only through the Java API. The library functions are implemented so that code safety checks are performed before certain system calls are executed. A safety policy is defined by providing code for the checkOperation methods in a SecurityManager subclass.

Policies that can be enforced by the Java Sandbox are limited by where the Java API calls check methods in the SecurityManager. For example, there is a checkConnect method that is called whenever an API method opens a socket connection, so we can define arbitary policies constraining what socket connections may be opened. However, there is not checkSend method, so we cannot define any policy that constrains what may be sent through a socket connection once it has been opened.

Naccio associates safety checks with abstract resource manipulations, so it can define policies that constrain any resource manipulation that is described by a resource description operation.

Can Naccio enforce a policy that ...?

Naccio can enforce any policy that can be implemented using the JDK Security Manager. An easy proof of this, is that we have written a Naccio policy, MimickJDK, that calls the same SecurityManager methods as the Java API would normally.

In addition, Naccio can enforce policies that constrain resources not considered by the JDK Security Manager, and can constrain those resources in more precise ways. Some examples of properties Naccio can enforce include:

• A limit on the total number of bytes that may be written by the program
• A constraint on the bandwidth the application may consume (by either raising a violation when the rate is exceeded, or by delaying network sends to satisfy the desired rate)
• A prohibition on transmitting your unencrypted credit card number over the Internet
• A requirement that all windows that receive mouse events have a warning string in their title bar
• A limit on the number of bytes the execution can write that is a function of the number of bytes it has read and the day of the week
• A limit on the number of threads or windows an execution may create.

Browse the policy library to see how some example policies are defined.

Some classes of properties Naccio cannot enforce (or cannot enforce without substantial difficulty) are:

Memory and CPU limits. Since memory and CPU usage is not directly tied to particular system calls, we cannot define a resource with operations corresponding directly to using memory of the CPU. The best we could do is approximate the resource operations by instrumenting the code to periodically call a RMemory.checkMemoryUsage operation and providing a RMemory.getMemoryUsage observer that would determine in a platform-dependent way how much memory is being used at the execution point. We could express safety policies as wrappers for the RMemory.checkMemoryUsage operation, however they can only be enforced approximately or at prohibative expense if we instrument the code to call RMemory.checkMemoryUsage after every instruction that may effect memory usage. Although its possible to do this, it seems more reasonable to enforce safety policies on memory and CPU usage directly in the run-time environment.

Information Flow. Naccio can easily enforce coarse-grain information flow security policies such as, "no data may be transmitted over the network after a sensitive file has been read". Supporting more precise information flow security policies, however, requires a deeper static analysis of programs than is done by Naccio.

Persistent safety properties. Naccio has no direct way of placing direct constraints across multiple program executions. We could attempt to do this in an ad hoc way by placing relevant state in a secure file that is read at the beginning of an execution, but there is no easy way to express properties that persist accross multiple executions.

Isn't it expensive to keep policy-specific versions of the platform library?

What does ... have to say about code safety?

Dave Barry

"And while we must recognize that computers are wonderful machines that have improved our lives in countless ways, we must also, by the same token, recognize that they are the evil demon spawn of hell."

From Come the millennium, use the stairs.

Bill Gates

"But software doesn't kill you."

Response when asked by CNN why GM recalls faulty cars and Microsoft sells upgrades.

The JDK License

"[This] Software is not designed or intended for use in on-line control of aircraft, air traffic, aircraft navigation or aircraft communications; or in the design, construction, operation or maintenance of any nuclear facility. Licensee warrants that it will not use or redistribute the Software for such purposes."

Java JDK Noncommercial Use License, 5.3.

William Shakespeare

"I would give all my fame for a pot of ale and safety."

King Henry V, Act iii, Scene 2.

Are you looking for a job?

Not anymore.

David Evans has accepted a position as an assistant professor at the University of Virginia. He will start there sometime this millenium or the next one.

I'm pretty sure I'm going to let [Bayern Munich's invitation] pass. ... I'm going back to school.

Chris Albright, US U-20 national team star and UVA student, quoted in Soccer America, May 10, 1999 issue. (Note: Dave didn't receive any offers from Bayern Munich.)

Andrew Tywman will graduate from MIT with an MEng degree in June 1999, and has accepted a position with Maker Communications.

Didn't answer your question?

Send mail to evans@virginia.edu.

Naccio Home Page
David Evans
University of Virginia, Computer Science