Bluish Coder

Building Wasp Lisp and MOSREF for Android

Wasp Lisp is a small cross platform lisp by Scott Dunlop that I've written about before and MOSREF is the secure remote injection framework that is one of the applications written with it.

I've been wanting to get Wasp running on Android and Gonk (the low level Android layer of Firefox OS) for debugging and small applications. One of the nice features of Wasp is being able to have a minimal interpreter running on a platform and send byte code from another system to that interpreter which is loaded and run. You can even send the bytecode compiler itself to be loaded and run in the interpreter to get a full system on the target. This is the basis of how MOSREF works where the drone gets sent code to run from the console system.

Standalone Toolkit

Building Wasp for Android requires generating a standalone toolchain from the Android NDK. This results in a vesion of gcc and libraries that can be run from conventional makefiles and configure scripts.

To generate a standalone toolchain to build Wasp I used:

$NDK_ROOT/build/tools/make-standalone-toolchain.sh \
      --platform=android-8 \
      --install-dir=$STK_ROOT

Replace NDK_ROOT with the path to the Android SDK and STK_ROOT with the destination where you want the standalone toolkit installed. The android-8 in the platform makes the standalone toolkit generate applications for FroYo and above (See STABLE-APIS.html.

Adding $STK_ROOT/bin to the PATH will make the compiler available:

export PATH=$PATH:$STK_ROOT/bin

Building libevent for Android

The Wasp virtual machine uses libevent to enable asynchronous operations. Building this for Android using the standalone toolkit is straightforward:

wget https://github.com/downloads/libevent/libevent/libevent-2.0.21-stable.tar.gz
tar xvf libevent-2.0.21-stable.tar.gz
cd libevent-2.0.21-stable
./configure --host=arm-linux-androideabi --prefix=$STK_ROOT
make
make install

This configures libevent to be built using the ARM compilers in the standalone toolkit and to install the resulting libraries in the same install location as the toolkit. This makes it easy for other applications to find and link with the library.

Building the Wasp stub for Android

A Wasp VM stub file is used for generating Wasp applications. The bytecode for an application is appended to the stub file and the result made to be executable. By having stubs for various operating systems and architectures you can create executables specific to them easily. To build the Android stub:

git clone git://github.com/swdunlop/WaspVM.git
cd WaspVM
STRIP=arm-linux-androideabi-strip \
  CC=arm-linux-androideabi-gcc \
  CFLAGS="-I $STK_ROOT/include -L $STK_ROOT/lib" \
  ARCH=arm-linux \
  OS=android \
  make

To build we define the correct version of the build programs to compile for ARM and set the architecture and OS to stop the build system from picking up the host system version of these. The result is a waspvm-android-arm-linux stub in the stubs directory.

Creating the host Wasp programs

To easily create Wasp programs for different platforms we'll need versions of them for the host we are running on. By doing a 'clean' followed by a 'make' on the host we'll clean out the Android build files and rebuild what's needed for the host. The 'clean' process doesn't remove the stub file we created in the previous step which still allows us to do android Wasp programs.

make clean
make

This produces a waspvm-linux-x86_64 stub in my stubs directory. To generate the Wasp interpreter and other programs:

make repl

Exit out of the repl with (exit) and there will be a wasp, waspc and waspld program for the host system. Now we can make a version of wasp for Android:

cd mod    
../waspc -exe ../awasp -platform android-arm-linux bin/wasp.ms

The waspc command takes a stub file (defined by the platform or stub argument) and appends the bytecode resulting from the compilation of the Wasp lisp code given as an argument. wasp.ms is the source for the intepreter. The output is set as awasp which is our executable for running on Android. We can use a similar command for producing Android versions of the other Wasp programs. MOSREF for example:

../waspc -exe ../amosref -platform android-arm-linux bin/mosref.ms

Running on Android

Running these executables on Android involves pushing them to somewhere writeable on the phone. If you have a rooted Android device (or a Firefox OS device) you can push them pretty much anywhere. On my non-rooted Jellybean Galaxy Note 2 I'm limited to just /data/local/tmp:

adb push awasp /data/local/tmp
adb shell
cd /data/local/tmp
chmod 0755 awasp
./awasp
>> (+ 1 2 3)
:: 6

This gives you a running Wasp interpreter. To develop and do interesting things on the phone you really need the Wasp mod files and the stub files copied over:

adb push mod /data/local/tmp
adb push stubs /data/local/tmp
adb shell
cd /data/local/tmp
./awasp
>> (import "lib/http-client")
:: #t
>> (http-response-body (http-get "http://icanhazip.com/"))
:: "xxx.xxx.xxx.xxx\n"
>> (exit)

MOSREF Android drone

It's simple now to create a MOSREF drone that runs on Android. Make sure the MOSREF console has a stubs directory containing the Android stub then create the drone as:

console> drone drone1 myphone android-arm-linux
Drone executable created.
Listening for drone on 10000...

Copy the created drone1 onto the phone and run it:

adb push mod/drone1 /data/local/tmp
adb shell
cd /data/local/tmp
chmod 0755 drone1
./drone1

Now on the console you can see the drone on the phone:

console> nodes
NODES: console online address: 192.168.1.101 port: 10000
       myphone online
console> on myphone sh ls
...directory listing...
console on myphone do (print "hello\n")
...prints hello on the phone 'adb shell' session...
console> on myphone load lib/http-file-server.ms
:: spawn-http-file-server
console> on myphone do (offer-http-file 8080 "/test" "text/plain" "Hello world!")
:: [queue 1F5DD00]

The load command shown above loads and compiles the Wasp lisp file on the host and sends the compiled bytecode to the drone on the phone. We then run the lisp code on the phone to start an HTTP server to serve data.

Ranged integer types and bounds checking

There's a discussion going on in the Rust mailing list about ranged integer types and whether they're useful for safety. Some of the points raised have been about the performance costs of dynamic bounds checks and the overhead of code for static bounds checks. I thought I'd write a post with my experiences with overfow checking in Gecko and with programming languages that can do overflow checking at compile time.

Gecko

There have been places in Gecko (the core Firefox engine) where overflow detection at compile time would be useful. An example is in the WAV audio format reading code. In this C++ code we have the following code:

static const int64_t BLOCK_SIZE = 4096;
int64_t readSize = std::min(BLOCK_SIZE, remaining);
int64_t frames = readSize / mFrameSize;

const size_t bufferSize = static_cast<size_t>(frames * mChannels);
nsAutoArrayPtr<AudioDataValue> sampleBuffer(new AudioDataValue[bufferSize]);

Here frames * mChannels can overflow with the result of the memory buffer allocated following it being of the wrong size and a memory access error occurring later. We can do a run time check that it won't overflow but this is error prone if someone changes BLOCK_SIZE to be of a size that causes overflow, or the size of AudioDataValue changes to do the same. It'll take an edge case in a test to find the problem. Better is to ensure that it will never overflow at compile time. The PR_STATIC_ASSERT construct can do this for us:

PR_STATIC_ASSERT(uint64_t(BLOCK_SIZE) < UINT_MAX / sizeof(AudioDataValue) / MAX_CHANNELS);
const size_t bufferSize = static_cast<size_t>(frames * mChannels);
nsAutoArrayPtr<AudioDataValue> sampleBuffer(new AudioDataValue[bufferSize]);

Now if BLOCK_SIZE, AudioDataValue or MAX_CHANNELS changes it will complain if the result overflows at compile time. Because C++ doesn't have dependent types and constraint solving, we don't have the ability to statically confirm that frames * mChannels avoids overflow automatically. We have to encode how those values are calculated in the PR_STATIC_ASSERT but it's better than nothing.

Similar code follows to check readSize:

PR_STATIC_ASSERT(uint64_t(BLOCK_SIZE) < UINT_MAX / sizeof(char));
nsAutoArrayPtr<char> dataBuffer(new char[static_cast<size_t>(readSize)]);

We encode the rule that BLOCK_SIZE must not be greater than UINT_MAX knowing that readSize is capped at BLOCK_SIZE.

Other uses of PR_STATIC_ASSERT are in that same file and various other places in the codebase. For example, Bug 623998. This was caused by an overflow in the implementation of the C++ operator new so we used PR_STATIC_ASSERT to ensure that the argument passed to operator new couldn't overflow based on analysis of the constraints of the arguments we pass to it.

ATS

The ATS programming language has a dependent type system that allows expressing ranges for integers at the static level. Unfortunately the current implementation uses machine integers in the constraint solver and this prevents easily expressing constraints involving overflow.

The Applied Operating System, an operating system kernel written in ATS, uses a patched ATS that uses libgmp for constraint solving and it declares types such overflow causes a type error. For example, the following code will not typecheck:

fun test () = {
  val a = ubyte1_of 250
  val c = ubyte1_of 6

  val d = a + b
}

The type checker recognizes that a is the exact unsigned byte value of 250 and that c is the exact type value of unsigned byte 6. Adding these together causing a byte greater than 255 which is a type error.

Constraints on types are propogated as expected. For example:

fun add_me {a,b: Ubyte} (a: ubyte a, b: ubyte b): ubyte (a+b) = a + b

fun test () = {
  val x = add_me (ubyte1_of 200, ubyte1_of 10)  
}

Here the arguments to add_me cannot be determined statically (assume test and add_me are compiled seperately so the compiler does not know the exact values at compile time) and the type checker will complain about the a+b since it can't prove that any unsigned byte added to another unsigned byte is less than the maximum value of an unsigned byte.

A solution is to add to the static system to say that the arguments to add_me add up to less than 255 and will not overflow and make callers check the range before calling:

fun add_me {a,b: Ubyte | a+b <= 255 } (a: ubyte a, b: ubyte b): ubyte (a+b) 
  = a + b

fun test () = {
  val x = add_me (ubyte1_of 200, ubyte1_of 10)  
}

With judicious use of constraints you can then push out the range check from the inner loops to the callers at the outmost region to reduce overhead. Or you can add dynamic checks close to the inner loops to reduce the burden on callers. The good thing is the compiler tells you when you get it wrong.

ATS2

ATS2 is a work in progress with improvements and additions to ATS. You'll need a recent version of ATS to build and then follow the instructions to get a working ATS2.

One of the improvements in ATS2 is allowing using libgmp to deal with constraints so range checks can be done to detect overflow. Hongwei Xi posted to the mailing list an example of using this to detect integer overflow in bsearch at compile time. This file can be typechecked with:

patsopt -tc -d doc/EXAMPLE/MISC/arith_overflow.dats

The arith_overflow example starts off by declaring an abstract type, intb to represent bounded integers:

abst@ype intb (i: int) // bounded integers

The type is indexed over a sort int. This is a dependent type that represents the value of the bounded integer. Cast functions are provided to allow converting between a normal integer and a bounded integer:

castfn intb2int {i:int} (i: intb i): int (i)
castfn int2intb {i:int | isintb(i)} (i: int i): intb (i)

The int2intb cast function has a contraint on its type index saying that the given integer is a bounded int via the isintb call. This is defined as:

stacst INTMIN : int and INTMAX : int
stadef isintb (i:int): bool = (INTMIN <= i && i <= INTMAX)
praxi lemma_INTMINMAX (): [INTMIN < ~0X7FFF ; INTMAX >= 0x7FFF] void

The way this works is two sorts constants are declared, INTMIN and INTMAX. The definition isintb constrains the index i to be between these two values. The values are not yet defined so all the type system knows for now is that isintb returns true if the given number is between two other numbers.

The axiom (introduced with praxi and is equivalent to a prfun or proof function) lemma_INTMINMAX states that INTMIN is < -0x&FFFF and INTMAX >= 0x7FFF. Once this proof function is called it tells the constraint system what the intb is bounded by.

Basic mathematic operations are provided for a bounded integer and the standard mathematical operators are overloaded with these. For example, adding two bounded integers:

fun add_intb_intb {i,j:int | isintb(i+j)} (i: intb (i), j: intb (j)):<> intb (i+j)
overload + with add_intb_intb

This is similar to the add_me function shown previously using the modified ATS compiler. It adds two bounded ints with the contraint that the result must also be a bounded int. Because the type system uses libgmp for the contraints it is able to ensure that the type system itself doesn't overflow when doing this check.

With these definitions for bounded ints in place it's possible to write code that will not typecheck if overflow occurs. The example in arith_overflow implements bsearch. Within the bsearch implementation it has the follow code:

val m = (l + r) / 2

Here l and r are bounded ints. Adding l and r can overflow and this will fail to compile. Changing the code to do effectively the same thing but avoiding adding the two numbers to prevent overflow results in compiling because the type checker can prove no overflow occurs:

val m = l + half (r - l)

Where half is defined to return the number divided by two:

fun half_intb {i:nat} (i: intb (i)):<> intb (ndiv(i,2))
overload half with half_intb

Summary

I think overflow checking at the type level is a very useful feature. It helps find important bugs early as people hardly ever check for overflow. When they do it's at runtime and the code is often not exercised until an issue actually occurs so may not handle things correctly.

For Mozilla C++ code we can use PR_STATIC_ASSERT (or preferably the recently introduced MOZ_STATIC_ASSERT) to help get some of the benefits of compile time overflow checking.

Social Engineering Attempt Warning

This morning when I checked my email I got a nice email from my server hosting provider titled "Root password reset". That's not usually a good sign when you haven't done any password resets recently.

The email was a service request response from the provider asking for confirmation to reset the root account on my server. I responded that this appeared to be a hack attempt, got online to chat with them and got the details of what happened.

An attacker had registered a domain, chrisdouble.co.nz, this morning. They rang my hosting provider to say they were me, and to reset the email address in my account to that domain. They managed to convince them to do this.

Once that was done they were able to get into the customer service portal for the server. No server maintenance could be done there but they got access to my phone number, billing details and the ability to raise service requests.

They raised a service request to reset the root password on the server. The service response was that they couldn't do this as the server was set up to use SSH keys and passwords were disabled. The attackers response to that was to ask them to physically access the server and re-enable password logins.

The support person emailed back to confirm this request but the email to the attackers domain bounced. They then emailed the previous address, which is my real email, and that was the one I read this morning.

While I was talking to the support person to resolve the issue the attacker was on the phone with this hosting company as well, trying to prove their identity as me. They had a number of personal details and it seemed to be a pretty well thought out social engineering attempt. In the end they realised we were fishing for information from them and they hung up.

It is amazing how close they got to being able to gain access to the server. If I hadn't been awake to read that email and respond quickly support would most likely have given them access. I've now arranged a protocol with them to prevent this from happening again.

If anyone I know receives an email or contact from chrisdouble.co.nz it is not me. If you are unsure you can ask for me to sign a message with GPG. My GPG fingerprint can be obtained by contacting me directly. Because the attacker gained access to the service portal they have a reasonable amount of identifying information (address, phone number, date of birth, etc). Don't take any of these as information to confirm an unusal contact as being me.

Backing up Gmail messages with offlineimap

A while back I realised I had a ton of email archived on Gmail which I would be sad to lose if I lost access to my Google account or couldn't access the internet for some reason. I also wanted a backup in case I decided to migrate away from Gmail to use another service.

The approach I took was to use offlineimap to download the contents of my mail using Gmail's IMAP support. I set it up to download a few days of email at a time so I wouldn't encounter any bandwidth limiting from Google or risk getting my account temporarily suspended for aggressive use.

I chose to use 'Maildir' format for the downloaded mail so I could use notmuch locally to read and search.

The matter of dealing with Gmail folders is a bit tricky. These are exposed as IMAP folders and if you're not careful you can end up downloading emails multiple times for each folder. I didn't really want the folder structure. I just wanted all emails and I'd use the tagging mechanism of notmuch to add tags after the fact.

The secret to ignoring folders is to create a folderfilter entry in the .offlineimaprc file. This is a lambda function that given a folder name should return true if it's a folder you want to be downloaded by offlineimap. I use:

folderfilter = lambda foldername: foldername in ['[Gmail]/All Mail', '[Gmail]/Sent Mail']

This downloads "All Mail" and "Sent Mail". This way I get everything in my Gmail without the folder structure.

I chose to add a nametrans entry so that the downloaded folders in the Maildir have more relevant names. nametrans is a lambda function that, given a folder name, returns the name that should be used locally for that folder. Here I translate "All Mail" to "all" and "Sent Mail" to "sent":

nametrans = lambda foldername: 
              re.sub('^[Gmail]/All Mail$', 'all', 
              re.sub('^[Gmail]/Sent Mail$', 'sent',foldername))

To connect to Gmail the following entries are used in the remote repository section:

type = Gmail
remotehost = imap.gmail.com
realdelete=no
maxconnections=1
ssl = yes
cert_fingerprint = 6d1b5b5ee0180ab493b71d3b94534b5ab937d042
remoteport = 993
remoteuser = ...
remotepass = ...

My local repository section is:

type = Maildir
localfolders = ~/.Mail

To prevent having to run offlineimap for a long time on the initial sync I did it over a series of days. I used the maxage setting in the Account section. When set mail older than this number of days is not synced. So I'd set it for 100 days, do a sync. Then I'd increase it by a 100 the next day and do another sync. Over a series of days/weeks I have all my email. Once completely synced I removed the entry from the .offlineimaprc file. I'm not sure what the best value is and maybe it doesn't matter but this worked for me.

My .offlineimaprc then looks like:

[general]
accounts = gmail
ui = TTY.TTYUI

[Account gmail]
localrepository = gmailLocal
remoterepository = gmailRemote
maxage = 1000

[Repository gmailLocal]
type = Maildir
localfolders = ~/.Mail

[Repository gmailRemote]
type = Gmail
remotehost = imap.gmail.com
realdelete=no
maxconnections=1
ssl = yes
cert_fingerprint = 6d1b5b5ee0180ab493b71d3b94534b5ab937d042
remoteport = 993
remoteuser = ...
remotepass = ...
nametrans = ...show above...
folderfilter = ...show above...

I used notmuch to process and search the Maildir locally. By setting synchronize_flags=true in my .notmuch-config file I could read the offline email in notmuch, incrementally sync with offlineimap, and the 'read', 'replied', etc flags are synchronized between them.

To tag with notmuch I run a script after syncing with .offlineimap that tags based on certain criteria. Something like:

offlineimap
notmuch new
notmuch tag +sent -- folder:sent and not tag:sent 
notmuch tag +bugzilla -inbox -- tag:inbox and from:bugzilla-daemon@mozilla.org
notmuch tag +ats -inbox -- tag:inbox and to:ats-lang-users
...etc...

Running Firefox OS on Nexus S

Update: 2013-05-07: Minor changes to deal with new and rebased patches.

Last year I posted about how to build and run B2G on the Nexus S. Much has changed since then and this post attempts to provide up to date instructions on building Firefox OS and installing the latest Gaia version.

I wrote 'attempts' because the support for the Nexus S bitrots frequently due to (I assume) most development effort going towards developer devices and devices that intend to be shipped. These instructions worked for me on my Nexus S and gives me a phone that can use Wifi, make calls, use 3G data, take photo's, record video and install applications.

Getting the source

The main source repository is on github, https://github.com/mozilla-b2g/b2g. The first step is to clone this repository. I clone this into a directory called nexus-s:

$ git clone git://github.com/mozilla-b2g/B2G nexus-s
$ cd nexus-s

Create a file in this directory called .userconfig containing the following:

export CC=gcc-4.6
export CXX=g++-4.6
export HIDPI=1

The first two entries are required if you are building on Ubuntu 12.10 to use gcc version 4.6, which you must install. B2G does not build using gcc version 4.7.

The last entry, HIDPI, results in applications using the correct resources for the screen size on the Nexus S. Without this many things will be scaled incorrectly.

Configuring

Once the source is obtained you need to pull down the sub-repositories required for the Nexus S. This step downloads multiple gigabytes of data and can take a long time:

nexus-s$ BRANCH=v1-train ./config.sh nexus-s

Note the use of the BRANCH environment variable. This configures our build to use the relatively stable v1-train branch. This branch gets regular updates but tends to be better tested than master which is often broken for not-quite-supported devices like the Nexus S.

Although we are using the v1-train we are going to use the master branch of Gaia so we get the latest and greatest user interface. We'll change to this later.

Gecko changes

The branch of Gecko that v1-train uses has some bugs on the Nexus S. To fix this we need to apply some patches. The first is bug 832653, video playback broken on Nexus S. The patches relevant to Gecko from this bug that need to be applied are:

• Fix graphic buffer crash

The following set of commands downloads these patches and applies them in a branch of the Gecko tree that the config.sh step previously obtained:

nexus-s       $ cd gecko
nexus-s/gecko $ git checkout -b nexus-s m/v1-train
nexus-s/gecko $ curl -k -L https://bug832653.bugzilla.mozilla.org/attachment.cgi?id=734988 >p1.patch
nexus-s/gecko $ patch -p1 <p1.patch
nexus-s/gecko $ git commit -a -m "Nexus S patches"
nexus-s/gecko $ cd ..

Gonk changes

Part of bug 832653 makes a change to the low level Gonk layer of B2G. This is in the libstagefright video decoding libraries. The change is to prevent output buffer starvation which results in video decoding stopping after a few frames. The required patch is:

• Fix output buffer starvation

To apply this patch:

nexus-s                 $ cd frameworks/base
nexus-s/frameworks/base $ git checkout -b nexus-s 
nexus-s/frameworks/base $ curl -k -L https://bugzilla.mozilla.org/attachment.cgi?id=735002 >p1.patch
nexus-s/frameworks/base $ patch -p1 <p1.patch
nexus-s/frameworks/base $ git commit -a -m "Nexus S patches"
nexus-s/frameworks/base $ cd ../..

Gaia changes

There are Gaia changes required as part of bug 869289 as well. This change prevents the error where videos are not listed if the thumbnail cannot be generated:

• List videos even if thumbnail generation fails

We also want to be on the Gaia master branch to get the latest and greatest code. The following comands switch to this branch and apply our patch:

nexus-s      $ cd gaia
nexus-s/gaia $ git checkout -b nexus-s mozillaorg/master
nexus-s/gaia $ curl -k -L https://bug869289.bugzilla.mozilla.org/attachment.cgi?id=746196 >p1.patch
nexus-s/gaia $ patch -p1 <p1.patch
nexus-s/gaia $ git commit -a -m "Nexus S video app thumbnail fix"

There is a bug related to video recording on the Nexus S. To fix this we need a patch from bug 832638:

• Set video recording profile in camera app

To apply this:

nexus-s/gaia $ curl -k -L https://bugzilla.mozilla.org/attachment.cgi?id=704241 >p2.patch
nexus-s/gaia $ patch -p1 <p2.patch
nexus-s/gaia $ git commit -a -m "Nexus S video recording fix"

Building

Now that all the required changes have been made we can build:

nexus-s $ ./build.sh 

Installing

Once the build is complete you should be able to flash the Nexus S with the results. Note that this completely wipes everything on your phone:

nexus-s $ ./flash.sh

The phone should reboot after this step with Firefox OS installed and prompting for information from the "First Run" app.

New Zealand changes

Some New Zealand sites don't detect Firefox OS and serve their mobile versions. This can be changed by adding overrides to gaia/build/ua-override-prefs.js. I add the entries in b2gnzuaoverride.txt to this file to get stuff.co.nz, mega.co.nz and trademe.co.nz serving the correct mobile site. Once added to this file, reinstall Gaia on the phone.

nexus-s $ ./flash.sh gaia

Updating

To update the source to latest versions we need to 'rebase' our changes on top of the most recent repository changes. The following steps will do this:

nexus-s $ git pull
nexus-s $ ./config.sh nexus-s
nexus-s $ cd gecko
nexus-s/gecko $ git rebase m/v1-train
nexus-s/gecko $ cd ../gaia
nexus-s/gaia  $ git rebase mozillaorg/master
nexus-s/gaia  $ cd ..
nexus-s $ ./build.sh

You may need to do some fixing up of merge conflicts if changes have occurred to the areas we've patched.

To flash the phone, overwriting everything on it, including all user data:

nexus-s $ ./flash.sh

To flash the phone, keeping (most of...) your existing user data:

nexus-s $ ./flash.sh system
nexus-s $ ./flash.sh gecko
nexus-s $ ./flash.sh gaia

Note that flashing gaia might remove some of your installed application icons. You'll need to reinstall those apps to fix that.