Safe TinyOS

What is Safe TinyOS?

Safe TinyOS is an alternate toolchain, released as part of TinyOS 2.1, that uses the Deputy compiler (now part of the Ivy project) to enforce type and memory safety at run time. Safety is useful for trapping impending memory errors.

Memory errors are particularly harmful on motes because

* Lacking virtual memory, safety errors are never trapped as segmentation violations.
* Since memory is tightly packed, the expected consequence of an array-bounds error is to corrupt RAM.
* Since deployed motes are very difficult to debug, and since other failure modes exist (battery outage, connectivity failure, etc.) it can be very hard to tell when memory corruption is the root cause of a serious deployment problem.

The SenSys2007 paper and slides can be found at: Efficient Memory Safety for TinyOS.

Safe Overview

The information here has been taken from http://www.cs.utah.edu/~coop/safetinyos

In particular, if you are trying to figure out the meaning behind Deputy modifiers, (such as "ONE", "ONE_NOK", and the like), you should look at section "Understanding Safe Code".

Safe TinyOS

What is Safe TinyOS?

It is an alternate toolchain for TinyOS 2 that uses the Deputy compiler to enforce type and memory safety at run time. Safety is useful for trapping pointer and array errors before they cause nasty consequences. For a detailed description of Safe TinyOS, please see our SenSys 2007 paper and slides.

Our short-term goal is for this document to mostly disappear due to the various elements it describes being included in the default TinyOS distribution. The parts of the document that are left will be turned into a TEP.

Platforms currently supported:

Mica2 MicaZ TelosB

Supporting additional platforms is not hard. Iris and Intelmote2 will be supported soon. (need to add information about how to add new platforms).

Installation

See the instructions here.

Usage

A standard TinyOS make invocation like "make micaz" will compile an unsafe application. To compile a safe application go to for example $TOSROOT/apps/Blink and run:

make [platform] safe

The safe version of Blink -- and all other applications that respect type and memory safety -- should act just like its unsafe equivalent.

Failure is Good

To see how trapping safety violations is useful, go to this directory:

$TOSROOT/apps/tutorials/BlinkFail Take a look inside BlinkFailC.nc. It is easy to see that the 11th time the Timer1.fired() is signaled, it will access out of bounds storage. First run the unsafe version:

make [platform] install Although the consequences of memory safety violations in C or nesC programs are arbitrary, the expected case is that RAM corruption will eventually cause the node to crash. In this case, a crash should happen after just a few seconds.

Now run the safe version:

make [platform] safe install The trapped safety violation is indicated by lots of LED activity. If you want to run this in Avrora: cp build/micaz/main.exe main.elf avrora -simulation=sensor-network -platform=micaz -monitors=leds,break,sleep,interrupts main.elf The Avrora output will contain text like this:

  0      54435382  break instruction @ 0x0B9E, r30:r31 = 0x0048
  0      54435382        @ deputy_fail_noreturn_fast
  0      54435382        @ deputy_fail_mayreturn
  0      54435382        @ VirtualizeTimerC$0$fireTimers
  0      54435382        @ AlarmToTimerC$0$fired$runTask

The value loaded into the Z register (r30:r31) in code from fail.c is the FLID (see below).

Interpreting Safety Violations

By default, a mote that encounters a safety violation repeatedly blinks a failure code on its LEDs. This code is a sequence of 8 digits each in the range 0-3. The read this code, wait for the mote's LEDs to "roll," or rapidly blink several times in a 1-2-3 sequence. Next, some number of LEDs will be lit-- write down this number. Usually the first digit or two of the FLID will be zero. Following each digit of the FLID, all three LEDs will be very briefly illuminated to serve as a separator. After all 8 digits have been presented the LEDs will roll and then the FLID is repeated. Once you have the sequence of 8 digits, it can be decoded as follows:

tos-decode-flid flid-file flid The flid-file argument specifies a file that helps the script map from the flid to an error message. Building a safe application causes this file to be placed here:

build/[platform]/flids.txt Mixing Safe and Unsafe Code

A module with the @safe attribute is compiled as type-safe and a module with the @unsafe attribute is compiled type-unsafe. By default, a module with neither of these attributes is considered unsafe. This default can be overridden using the nesC command line option -fnesc-default-safe.

TODO: explain how to find and eliminate unwanted trusted modules

Understanding Safe Code

Safe code contains safety annotations that are used to communicate invariants to the Deputy compiler so that it can insert appropriate safety checks. Most annotations appear in function prototypes and on global variables, but sometimes annotations are needed inside functions.

Annotations that you will find in TinyOS code are:

ONE -- a pointer that always refers to a single object, similar to a C++ reference ONE_NOK -- same as ONE but may be null COUNT(n) -- a pointer that always refers to a block of at least n objects COUNT_NOK(n) -- same as COUNT but may be null BND(n,m) -- a pointer p such that n≤p<m, and that is aligned with respect to n and m BND_NOK(n,m) -- same as BND but may be null TCAST(type,expr) -- a trusted cast, which tells Deputy to just trust the programmer. This is needed to perform casts that are inherently unsafe (e.g., casting an array of bytes into a message_t) or to perform casts that are safe but beyond the reach of Deputy's type system (e.g. some kinds of getHeader() and getFooter() calls) TRUSTEDBLOCK -- code that is completely trusted (i.e., ignored by Deputy). This is used in very few places, and should be avoided when possible. The non-null annotations should be used whenever possible, for two reasons. First, the are good documentation. Second, they can help Deputy produce better code since dereferences of these pointers need not be preceded by a null check.

Understanding Annotations in tos/interfaces/*.nc

Write me.

Writing Safe Code

Writing safe code is generally very easy: in the common case annotations are only needed on pointers that reference multiple objects. The best way to get started is to compile regular nesC or C code in safe mode, see what warnings/errors are emitted by the Deputy compiler, and then start annotating the code until it compiles cleanly. In a small minority of cases, it is necessary to do some refactoring.

Jeremy Condit's quick reference and manual for Deputy are the best starting points for learning to use its type system.

Customized Failure Handlers

The default safety violation handler is here: $SAFE_TINYOS_HOME/tinyos-2.x/tos/lib/safe/platform/fail.c This code can be changed to send a packet, log to flash, reboot the mote, or whatever you like. Note that it is highly unlikely that you could send a packet if a fault happened to occur in the radio stack. Optimization

These instructions give a binary that is not heavily optimized. It is possible to reduce the overheads of safety using our cXprop optimizer. We'll add instructions later on how to do this.

To Do

We have not yet, but plan to: Support platforms other than Mica2, Micaz, and TelosB Make TOSSIM work in safe mode Integrate Safe TinyOS with a stack depth analysis tool to avoid unsafety through stack overflow Solve the problem of unsafe accesses to pointers to dead stack frames -- these are not covered by Deputy

Write documentation Eliminate as much trusted code (TCAST and TRUSTEDBLOCK) as possible Let us know if you'd like to help!

Feedback

Please send problem reports and other feedback to directly to John Regehr or to one of the TinyOS mailing lists. We can create a mailing list specific to Safe TinyOS if that seems desirable. People

We are John Regehr, Eric Eide, Nathan Cooprider, Will Archer, and Yang Chen at Utah, and David Gay at Intel Research Berkeley.

Acknowledgments

The Deputy and CIL people at Berkeley, mainly Jeremy Condit (now at Microsoft Research), Matt Harren, and Zachary Anderson, have been extremely helpful.

This work has benefited from input from the TinyOS 2 Core Working Group. In particular, Phil Levis pushed through an important change to the getPayload interface.

This work is supported by NSF awards CNS-0615367 and CNS-0448047.