Safe TinyOS
Contents
- 1 What is Safe TinyOS?
- 2 Supported Platforms
- 3 Building a Safe Application
- 4 Interpreting Safety Violations
- 5 Safety Violations in a Simulator
- 6 Understanding Safe Code
- 7 Understanding Annotations in tos/interfaces/*.nc
- 8 Mixing Safe and Unsafe Code
- 9 Writing Safe Code
- 10 Customized Failure Handlers
- 11 To Do
- 12 Feedback
- 13 Acknowledgments
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 on motes. Together, type and memory safety give Java-like guarantees to TinyOS programs: pointer and array errors are trapped before they occur.
Untrapped memory errors are particularly harmful on motes because
- Lacking memory protection hardware and a user/kernel boundary, it is easy to accidentally corrupt OS code; these errors are never trapped as segmentation violations.
- Since memory objects are tightly packed, walking even one element past the end of an array is likely to corrupt RAM.
- Since deployed motes are 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.
Safe TinyOS is described in detail in a paper from SenSys 2007: Efficient Memory Safety for TinyOS.
Supported Platforms
Safe compilation is supported by default by TinyOS 2.1 for these platforms:
- Mica2
- MicaZ
- TelosB
TODO: We'd like to support Iris, Intelmote2, Shimmer. Patches appreciated.
Building a Safe Application
Getting started is easy. To compile a safe application go to for example $TOSROOT/apps/Blink and run:
make micaz safe
Since Blink contains no known safety errors, the safe version of Blink should act just like its unsafe counterpart.
As a sanity check, make sure that the code size of the safe version of Blink is larger than that of the unsafe version:
$ make micaz mkdir -p build/micaz compiling BlinkAppC to a micaz binary ncc -o build/micaz/main.exe .... compiled BlinkAppC to build/micaz/main.exe 2052 bytes in ROM 51 bytes in RAM avr-objcopy --output-target=srec build/micaz/main.exe build/micaz/main.srec avr-objcopy --output-target=ihex build/micaz/main.exe build/micaz/main.ihex writing TOS image $ make micaz safe mkdir -p build/micaz compiling BlinkAppC to a micaz binary ncc -o build/micaz/main.exe ... compiled BlinkAppC to build/micaz/main.exe 2562 bytes in ROM 51 bytes in RAM avr-objcopy --output-target=srec build/micaz/main.exe build/micaz/main.srec avr-objcopy --output-target=ihex build/micaz/main.exe build/micaz/main.ihex writing TOS image
As illustrated here, Safe TinyOS does not have any RAM overhead. The ROM overhead is due to bounds-checking code inserted by the Deputy compiler.
Interpreting Safety Violations
TinyOS 2.1 comes with an application that is designed to fail; it is here:
$TOSROOT/apps/tutorials/BlinkFail
Looking at 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 of this application:
make micaz install
In general, it is hard to predict the consequences of a memory safety violation in a TinyOS program. In many cases, the observable symptom is node crash. That is what should happen after running the unsafe BlinkFail for a few seconds.
Next run the safe version:
make micaz safe install
Prior to accessing a[10], the Safe TinyOS failure handler is invoked, resulting in lots of LED activity. The purpose of this activity is to give you a "FLID" (fault location identifier) indicating the source-code location of the faulting access.
A FLID is a sequence of 8 base-4 digits. To read a FLID, 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 a 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 again 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
Safety Violations in a Simulator
A simulator offers a pleasant alternative to debugging safety violations on real hardware. To try this out, first download and install the CVS version of Avrora.
Next: build a safe version of BlinkFail, make a copy with the .elf extension, and run it in Avrora:
make micaz safe cp build/micaz/main.exe main.elf java avrora.Main -simulation=sensor-network -platform=micaz -monitors=leds,break,sleep,interrupts main.elf
The Avrora output should 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 callstack leading up to the safety violation is shown. The value loaded into the register pair r30:r31 (the AVR's Z register) is the FLID.
TODO: We'd like an Avrora monitor that goes ahead and automatically decodes the FLID.
TODO: We'd like analogous instructions for mspsim.
Understanding Safe Code
Safe code contains annotations that express invariants in such a way that the Deputy compiler can perform appropriate static and dynamic checking. 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 generally result in more efficient code since dereferences of these pointers need not be preceded by a NULL check.
Understanding Annotations in tos/interfaces/*.nc
Write me.
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
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 groups 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. This work is supported by NSF awards CNS-0615367, CNS-0448047, and CNS-0410285.