Preventing heartbleed bugs with safe programming languages

The Heartbleed bug in OpenSSL has resulted in a fair amount of damage across the internet. The bug itself was quite simple and is a textbook case for why programming in unsafe languages like C can be problematic.

As an experiment to see if a safer systems programming language could have prevented the bug I tried rewriting the problematic function in the ATS programming language. I've written about ATS as a safer C before. This gives a real world testcase for it. I used the latest version of ATS, called ATS2.

ATS compiles to C code. The function interfaces it generates can exactly match existing C functions and be callable from C. I used this feature to replace the dtls1_process_heartbeat and tls1_process_heartbeat functions in OpnSSL with ATS versions. These two functions are the ones that were patched to correct the heartbleed bug.

The approach I took was to follow something similar to that outlined by John Skaller on the ATS mailing list:

ATS on the other hand is basically C with a better type system.
You can write very low level C like code without a lot of the scary
dependent typing stuff and then you will have code like C, that
will crash if you make mistakes.

If you use the high level typing stuff coding is a lot more work
and requires more thinking, but you get much stronger assurances
of program correctness, stronger than you can get in Ocaml
or even Haskell, and you can even hope for *better* performance
than C by elision of run time checks otherwise considered mandatory,
due to proof of correctness from the type system. Expect over
50% of your code to be such proofs in critical software and probably
90% of your brain power to go into constructing them rather than
just implementing the algorithm. It's a paradigm shift.

I started with wrapping the C code directly and calling that from ATS. From there I rewrote the C code into unsafe ATS. Once that worked I added types to find errors.

I've put the modified OpenSSl code in a github fork. The two branches there, ats and ats_safe, represent the latter two stages in implementing the functions in ATS.

I'll give a quick overview of the different paths I took then go into some detail about how I used ATS to find the errors.

Wrapping C code

I've written about this approach before. ATS allows embedding C directly so the first start was to embed the dtls1_process_heartbeat C code in an ATS file, call that from an ATS function and expose that ATS function as the real dtls1_process_heartbeat. The code for this is in my first attempt of d1_both.dats.

Unsafe ATS

The second stage was to write the functions using ATS but unsafely. This code is a direct translation of the C code with no additional typechecking via ATS features. It uses usafe ATS code. The rewritten d1_both.dats contains this version.

The code is quite ugly but compiles and matches the C version. When installed on a test system it shows the heartbleed bug still. It uses all the pointer arithmetic and hard coded offsets as the C code. Here's a snippet of one branch of the function:

val buffer = OPENSSL_malloc(1 + 2 + $UN.cast2int(payload) + padding)
val bp = buffer

val () = $UN.ptr0_set<uchar> (bp, TLS1_HB_RESPONSE)
val bp = ptr0_succ<uchar> (bp)
val bp = s2n (payload, bp)
val () = unsafe_memcpy (bp, pl, payload)
val bp = ptr_add (bp, payload)
val () = RAND_pseudo_bytes (bp, padding)
val r = dtls1_write_bytes (s, TLS1_RT_HEARTBEAT, buffer, 3 + $UN.cast2int(payload) + padding)
val () = if r >=0 && ptr_isnot_null (get_msg_callback (s)) then
           call_msg_callback (get_msg_callback (s),
                              1, get_version (s), TLS1_RT_HEARTBEAT,
                              buffer, $UN.cast2uint (3 + $UN.cast2int(payload) + padding), s,
                              get_msg_callback_arg (s))
val () = OPENSSL_free (buffer)

It should be pretty easy to follow this comparing the code to the C version.

Safer ATS

The third stage was adding types to the unsafe ATS version to check that the pointer arithmetic is correct and no bounds errors occur. This version of d1_both.dats fails to compile if certain bounds checks aren't asserted. If the assertloc at line 123, line 178 or line 193 is removed then a constraint error is produced. This error is effectively preventing the heartbleed bug.

Testable Vesion

The last stage I did was to implement the fix to the tls1_process_heartbeat function and factor out some of the helper routines so it could be shared. This is in the ats_safe branch which is where the newer changes are happening. This version removes the assertloc usage and changes to graceful failure so it could be tested on a live site.

I tested this version of OpenSSL and heartbleed test programs fail to dump memory.

The approach to safety

The tls_process_heartbeat function obtains a pointer to data provided by the sender and the amount of data sent from one of the OpenSSL internal structures. It expects the data to be in the following format:

 byte = hbtype
 ushort = payload length
 byte[n] = bytes of length 'payload length'
 byte[16]= padding

The existing C code makes the mistake of trusting the 'payload length' the sender supplies and passes that to a memcpy. If the actual length of the data is less than the 'payload length' then random data from memory gets sent in the response.

In ATS pointers can be manipulated at will but they can't be dereferenced or used unless there is a view in scope that proves what is located at that memory address. By passing around views, and subsets of views, it becomes possible to check that ATS code doesn't access memory it shouldn't. Views become like capabilities. You hand them out when you want code to have the capability to do things with the memory safely and take it back when it's done.

Views

To model what the C code does I created an ATS view that represents the layout of the data in memory:

dataview record_data_v (addr, int) =
  | {l:agz} {n:nat | n > 16 + 2 + 1} make_record_data_v (l, n) of (ptr l, size_t n)
  | record_data_v_fail (null, 0) of ()

A 'view' is like a standard ML datatype but exists at type checking time only. It is erased in the final version of the program so has no runtime overhead. This view has two constructors. The first is for data held at a memory address l of length n. The length is constrained to be greater than 16 + 2 + 1 which is the size of the 'byte', 'ushort' and 'padding' mentioned previously. By putting the constraint here we immediately force anyone creating this view to check the length they pass in. The second constructor, record_data_v_fail, is for the case of an invalid record buffer.

The function that creates this view looks like:

implement get_record (s) =
  val len = get_record_length (s)
  val data = get_record_data (s)
in
  if len > 16 + 2 + 1 then
    (make_record_data_v (data, len) | data, len)
  else
    (record_data_v_fail () | null_ptr1 (), i2sz 0)
end

Here the len and data are obtained from the SSL structure. The length is checked and the view is created and returned along with the pointer to the data and the length. If the length check is removed there is a compile error due to the constraint we placed earlier on make_record_data_v. Calling code looks like:

val (pf_data | p_data, data_len) = get_record (s)

p_data is a pointer. data_len is an unsigned value and pf_data is our view. In my code the pf_ suffix denotes a proof of some sort (in this case the view) and p_ denotes a pointer.

Proof functions

In ATS we can't do anything at all with the p_data pointer other than increment, decrement and pass it around. To dereference it we must obtain a view proving what is at that memory address. To get speciailized views specific for the data we want I created some proof functions that convert the record_data_v view to views that provide access to memory. These are the proof functions:

(* These proof functions extract proofs out of the record_data_v
   to allow access to the data stored in the record. The constants
   for the size of the padding, payload buffer, etc are checked
   within the proofs so that functions that manipulate memory
   are checked that they remain within the correct bounds and
   use the appropriate pointer values
*)
prfun extract_data_proof {l:agz} {n:nat}
               (pf: record_data_v (l, n)):
               (array_v (byte, l, n),
                array_v (byte, l, n) -<lin,prf> record_data_v (l,n))
prfun extract_hbtype_proof {l:agz} {n:nat}
               (pf: record_data_v (l, n)):
               (byte @ l, byte @ l -<lin,prf> record_data_v (l,n))
prfun extract_payload_length_proof {l:agz} {n:nat}
               (pf: record_data_v (l, n)):
               (array_v (byte, l+1, 2),
                array_v (byte, l+1, 2) -<lin,prf> record_data_v (l,n))
prfun extract_payload_data_proof {l:agz} {n:nat}
               (pf: record_data_v (l, n)):
               (array_v (byte, l+1+2, n-16-2-1),
                array_v (byte, l+1+2, n-16-2-1) -<lin,prf> record_data_v (l,n))
prfun extract_padding_proof {l:agz} {n:nat} {n2:nat | n2 <= n - 16 - 2 - 1}
               (pf: record_data_v (l, n), payload_length: size_t n2):
               (array_v (byte, l + n2 + 1 + 2, 16),
                array_v (byte, l + n2 + 1 + 2, 16) -<lin, prf> record_data_v (l, n))

Proof functions are run at type checking time. They manipulate proofs. Let's breakdown what the extract_hbtype_proof function does:

prfun extract_hbtype_proof {l:agz} {n:nat}
               (pf: record_data_v (l, n)):
               (byte @ l, byte @ l -<lin,prf> record_data_v (l,n))

This function takes a single argument, pf, that is a record_data_v instance for an address l and length n. This proof argument is consumed. Once it is called it cannot be accessed again (it is a linear proof). The function returns two things. The first is a proof byte @ l which says "there is a byte stored at address l". The second is a linear proof function that takes the first proof we returned, consumes it so it can't be reused, and returns the original proof we passed in as an argument.

This is a fairly common idiom in ATS. What it does is takes a proof, destroys it, returns a new one and provides a way of destroying the new one and bring back the old one. Here's how the function is used:

prval (pf, pff) = extract_hbtype_proof (pf_data)
val hbtype = $UN.cast2int (!p_data)
prval pf_data = pff (pf)

prval is a declaration of a proof variable. pf is my idiomatic name for a proof and pff is what I use for proof functions that destroy proofs and return the original.

The !p_data is similar to *p_data in C. It dereferences what is held at the pointer. When this happens in ATS it searches for a proof that we can access some memory at p_data. The pf proof we obtained says we have a byte @ p_data so we get a byte out of it.

A more complicated proof function is:

prfun extract_payload_length_proof {l:agz} {n:nat}
               (pf: record_data_v (l, n)):
               (array_v (byte, l+1, 2),
                array_v (byte, l+1, 2) -<lin,prf> record_data_v (l,n))

The array_v view repesents a contigous array of memory. The three arguments it takes are the type of data stored in the array, the address of the beginning, and the number of elements. So this function consume the record_data_v and produces a proof saying there is a two element array of bytes held at the 1st byte offset from the original memory address held by the record view. Someone with access to this proof cannot access the entire memory buffer held by the SSL record. It can only get the 2 bytes from the 1st offset.

Safe memcpy

One more complicated view:

prfun extract_payload_data_proof {l:agz} {n:nat}
               (pf: record_data_v (l, n)):
               (array_v (byte, l+1+2, n-16-2-1),
                array_v (byte, l+1+2, n-16-2-1) -<lin,prf> record_data_v (l,n))

This returns a proof for an array of bytes starting at the 3rd byte of the record buffer. Its length is equal to the length of the record buffer less the size of the payload, and first two data items. It's used during the memcpy call like so:

prval (pf_dst, pff_dst) = extract_payload_data_proof (pf_response)
prval (pf_src, pff_src) = extract_payload_data_proof (pf_data)
val () = safe_memcpy (pf_dst, pf_src 
           add_ptr1_bsz (p_buffer, i2sz 3),
           add_ptr1_bsz (p_data, i2sz 3),
           payload_length)
prval pf_response = pff_dst(pf_dst)
prval pf_data = pff_src(pf_src)

By having a proof that provides access to only the payload data area we can be sure that the memcpy can not copy memory outside those bounds. Even though the code does manual pointer arithmetic (the add_ptr1_bszfunction) this is safe. An attempt to use a pointer outside the range of the proof results in a compile error.

The same concept is used when setting the padding to random bytes:

prval (pf, pff) = extract_padding_proof (pf_response, payload_length)
val () = RAND_pseudo_bytes (pf |
                            add_ptr_bsz (p_buffer, payload_length + 1 + 2),
                            padding)
prval pf_response = pff(pf)a

Runtime checks

The code does runtime checks that constrain the bounds of various length variables:

if payload_length > 0 then
    if data_len >= payload_length + padding + 1 + 2 then
    ...
...

Without those checks a compile error is produced. The original heartbeat flaw was the absence of similar runtime checks. The code as structured can't suffer from that flaw and still be compiled.

Testing

This code can be built and tested. First step is to install ATS2:

$ tar xvf ATS2-Postiats-0.0.7.tgz
$ cd ATS2-Postiats-0.0.7
$ ./configure
$ make
$ export PATSHOME=`pwd`
$ export PATH=$PATH:$PATSHOME/bin

Then compile the openssl code with my ATS additions:

$ git clone https://github.com/doublec/openssl
$ cd openssl
$ git checkout -b ats_safe origin/ats_safe
$ ./config
$ make
$ make test

Try changing some of the code, modifying the constraints tests etc, to get an idea of what it is doing.

For testing in a VM, I installed Ubuntu, setup an nginx instance serving an HTTPS site and did something like:

$ git clone https://github.com/doublec/openssl
$ cd openssl
$ git diff 5219d3dd350cc74498dd49daef5e6ee8c34d9857 >~/safe.patch
$ cd ..
$ apt-get source openssl
$ cd openssl-1.0.1e/
$ patch -p1 <~/safe.patch
  ...might need to fix merge conflicts here...
$ fakeroot debian/rules build binary
$ cd ..
$ sudo dpkg -i libssl1.0.0_1.0.1e-3ubuntu1.2_amd64.deb \
               libssl-dev_1.0.1e-3ubuntu1.2_amd64.deb 
$ sudo /etc/init.d/nginx restart

You can then use a heartbleed tester on the HTTPS server and it should fail.

Conclusion

I think the approach of converting unsafe C code piecemeal worked quite well in this instance. Being able to combine existing C code and ATS makes this much easier. I only concentrated on detecting this particular programming error but it would be possible to use other ATS features to detect memory leaks, abstraction violations and other things. It's possible to get very specific in defining safe interfaces at a cost of complexity in code.

Although I've used ATS for production code this is my first time using ATS2. I may have missed idioms and library functions to make things easier so try not to judge the verbosity or difficulty of the code based on this experiement. The ATS community is helpful in picking up the language. My approach to doing this was basically add types then work through the compiler errors fixing each one until it builds.

One immediate question becomes "How do you trust your proof". The record_data_v view and the proof functions that manipulate it define the level of checking that occurs. If they are wrong then the constraints checked by the program will be wrong. It comes down to having a trusted kernel of code (in this case the proof and view) and users of that kernel can then be trusted to be correct. Incorrect use of the kernel is what results in the stronger safety. From an auditing perspective it's easier to check the small trusted kernel and then know the compiler will make sure pointer manipulations are correct.

The ATS specific additions are in the following files:

• d1_both.dats
• t1_lib.dats
• shared.sats
• shared.dats
• shared.cats

Multiple Users in a Self World

One of the things I like about the Self programming language is it has lots of interesting old projects written in Self included in the source distribution. These include a Dylan interpreter, Cecil interpreter, web browser, and partial Java implementation amongst other things.

Once of the features Self has is the ability to allow remote users to connect to a Self instance running the Morphic user interface. This is usually done using X11's facility to share remote windows. But included in the Self source is a client written in Java and a server written in Self that allows remote users to connect using a Java Applet in a web browser.

The code for this has bitrot slightly but I've updated it just enough to work and demo. My fixes have been merged into the official Self repository on github.

Server side

With these changes and a build of Self you should start with a fresh image containing the Morphic code (UI2). From the self console run:

$ cd objects
$ ../Self 
"Self 1" 'applications/javaServer/loadJavaServer.self' _RunScript

This will load the server code. It's best to do this in a fresh instance as it modifies some UI objects that result in Self having to rebuild a number of dependencies for the objects in the system. This can make an existing system sluggish for a bit.

Once loaded, start the desktop:

"Self 2" desktop open

From a shell in the desktop, create a copy of the javaDaemon object using 'Get it' and put it somewhere:

javaDaemon copy

The outliner for this allows changing the port slot if needed, which defaults to 1420. Middle click on the outliner's title and choose 'Show Morph'. This creates a default tan square that can be placed anywhere. The world that this morph lives in is the world that remote users will connect to.

From the outliner run the start method. There will be a prompt warning you that this is a security issue as you're allowing remote access to your machine. Answering Yes will run the server.

Client side

The client code is written in Java. The source is in objects/applications/javaClient. The shell script BuildJavaClient will build the Java code. The Test.html page in that directory should be served from a web server and accessed by a web browser. Note that due to Java security settings this must be served from an actual web server. I used a local thttpd instance. There may also need to be some changing of Java Applet settings in the Java control panel to allow the applet to make socket connections.

Once 'Test.html' is loaded you can enter a username, keep the password empty, and connect. You should now see the Self desktop.

Usage

Unfortunately when the client connects sometimes the Self desktop stops and it won't respond. To restart it enter in the Self console:

desktop go

When this is done you'll see the remote users 'hand' (Self term for mouse pointer) in the Self desktop as an arrow with their name. A border will be in the world with the color of the user showing the extent of the desktop that the user can see in their remote session.

Dragging items around in both sessions is reflected in the world. Other users can connect too. The Java client uses 'Shift+Left Click' as the right mouse button and 'Control+Left Click' as the middle mouse button.

Demo

I did a short screencast of using the remote sharing to show how it works. If your browser supports HTML video it should show below.

Future

I think a dedicated protocol like this is probably better than using remote X11. Self currently is quite tied to X but if it could be moved off it it would allow easier porting to Windows, Android and other non-X platforms. Perhaps using something like SDL2 to get cross platform and hardware acceleration.

More information about the protocol and implementation of the Java client is available in JavaClientServerOverview.txt

An interesting project would to be port the javaClient code to JavaScript using an HTML canvas or WebGL to display the remote work. The server could be updated to communicate via HTTP, WebSockets, or even WebRTC's peer to peer facilities.

Running the Self Programming Language on Android

I've written about the Self programming language before and still occasionally fire up the GUI environment to explore prototype object development. The Self implementation is JIT based and doesn't have an interpreter. I've wanted to have the Self environment running on a mobile device but most tablets and phones are ARM based and Self doesn't have an ARM backend.

Intel based mobile devices are starting to appear however so I decided to try and get Self running on one. The GUI backend for Self on Linux uses X11 and it's a bit too large a project to do an Android GUI backend so I just tried getting the console REPL of Self working.

Building on Linux

My first step was to revive my port of the Self build system that uses Tup instead of the original custom shell scripts. By doing this I'd gain a better understanding of how Self is built and then move to using Android tools. My rebased version of Self that uses tup to build is in the tup branch of my Self github fork. With tup installed this can be built with (probably works on Linux only, sorry):

$ git clone https://github.com/doublec/self
$ cd self
$ git checkout -b tup origin/tup
$ tup init
$ tup upd

This creates a Self executable in the root of the Self checkout. A bootstrapped snapshot can be created with:

$ cd objects
$ ../Self 
Self Virtual Machine Version 4.1.13
Copyright 1989-2003: The Self Group (type _Credits for credits)

for I386:  LogVMMessages = true
for I386:  PrintScriptName  = true
for I386:  Inline = true
for I386:  SICDeferUncommonBranches = false (not implemented)
for I386:  SICReplaceOnStack = false (not implemented)
for I386:  SaveOutgoingArgumentsOfPatchedFrames = true
VM# 'worldBuilder.self' _RunScript

The 'worldBuilder.self' _RunScript command loads a script that loads the code for the standard Self runtime. It prompts if you want UI2, which you do if you want the GUI, and UI1, which you don't unless you want to explore the old gui.

Once loaded you can run some basic commands:

"Self 0" 'hello world' print
hello world'hello world'
"Self 1" 100 factorial.
a bigInt(9332621544394415...00000000000000000000)
"Self 2" [ 1000 factorial ] time.
1552
"Self 3" desktop open.

The last comand, desktop open, runs the Self GUI. You can see a screencast of me using the GUI in my displaying images with Self post.

Android Standalone Toolchain

To build Self for Android we need to generate a standalone toolchain from the Android NDK. To generate an x86 toolchain:

$ cd $NDK_HOME
$ ./build/tools/make-standalone-toolchain.sh  \
     --arch=x86 \
     --install-dir=/somewhere/stk

This generates the toolchain and copies it to the /somewhere/stk directory. That should be changed to where you want it installed and it needs to be added to the path:

$ export PATH=/somewhere/stk/bin:$PATH

Android ncurses

Self uses termlib from the ncurses library. This can be built from source and installed using the standalone toolchain:

$ wget http://ftp.gnu.org/pub/gnu/ncurses/ncurses-5.9.tar.gz
$ tar xvf ncurses-5.9.tar.gz
$ cd ../ncurses-5.9
$ ./configure --host=i686-android-linux \
              --prefix=/somewhere/stk \
              --with-termlib
$ make
$ make install

The prefix in the configure line above will install it in the location of the standalone toolchain so it can be found easily when building Self.

Android Self

I've generated a patch file that allows building Self in Android. It's pretty rough but gets the console REPL working and can then be fixed up later. To apply and build:

$ git clone https://github.com/doublec/self
$ cd self
$ git checkout -b tup origin/tup
$ curl http://bluishcoder.co.nz/self/android.patch | patch -p1
$ tup init
$ tup upd

The resulting executable should be pushed to a directory on the Android device. Pushing the objects directory will provide the files to allow bootstrapping the Self runtime system:

$ adb push Self /data/local/tmp
$ adb push objects /data/local/tmp
$ adb shell
device$ cd /data/local/tmp
device$ chmod 0755 Self
device$ ./Self
VM# 'worldBuilder.self' _RunScript

You can also run Self from within a terminal emulator. If you do this I recommend installing the Hacker's Keyboard as well.

Running the benchmark suite on my laptop gives about 2 seconds elapsed time. On the Asus Fonepad it's 10 seconds, so approximately 5x slower. The benchmark can be run with:

"Self 0" [ benchmarks run ] time

Binaries

A precompiled binary is available at i686-android-linux-Self.bz2. Uncompress it before copying it to the device. You'll need the objects directory from the git source to boostrap the runtime environment:

$ wget http://bluishcoder.co.nz/self/i686-android-linux-Self.bz2
$ bunzip2 i686-android-linux-Self.bz2
$ mv i686-android-linux-Self.bz2 Self
$ adb push Self /data/local/tmp
$ git clone https://github.com/doublec/self
$ cd self
$ git checkout -b tup origin/tup
$ adb push objects /data/local/tmp
...as previously to run...

Summary

This provides basic console Self usage. It requires knowing how to program in Self without using the GUI, which is not the most common way of writing Self programs. An interesting next exercise would be trying to get a GUI working.

The images below show Self running on two x86 Android devices. On the left is a screenshot of running on a Samsung Galaxy Tab 3 10.1 and on the right running on an Asus Fonepad with bluetooth keyboard. Click on the images for the larger version.

Unfortunately this build doesn't work on ARM as mentioned previously. I suspect an ARM backend would be a significant amount of work.

For more reading on Self:

• Self Handbook
• Self Papers
• Prototype Based Programming Languages
• Attack of the clones
• self-interest mailing list
• Self IRC channel is #self-lang on Freenode

HTML Media support in Firefox

Some time ago I wrote a dev-media post outlining the media formats we support and requesting discussion on future formats. This post summarizes the results of that and changes that have occurred since then.

In general Mozilla is trying to limit the proliferation of media formats on the web. One reason for doing this is to make it easier for a website to provide media that they know can be played by the majority of web users. Ideally the formats supported would be freely implementable by anyone in any user agent. This enables someone to share media on the web knowing that all users can watch it.

A counter argument is that limiting the formats to a small number restricts the producers of the media. They are unable to select the best formats for the type of media they are sharing that plays best on specific devices (for example, taking advantage of hardware acceleration on a device). The choice of what formats can be used would be left up to the operating system in this case and the browser would fall back to using operating system support when it wants to decode media data.

Taking the operating system codec approach would result in media on the web only being able to be played by a subset of users. If someone shares a wmv video file it will only play back on systems supporting that format. The list of all possible formats is huge and the intersection of formats supported across operating systems isn't great. We'd also like to avoid codec support on the web becoming a vector for malware. Evil sites could prompt users to install malware infected codecs required to play video from the site for example.

By building support for specific formats in the browser we hope to guarantee to media producers that their media will be viewable by all web users safely.

Firefox currently supports the following media formats where the decoding support is built into the browser:

• Opus audio in an Ogg container on all platforms.
• Vorbis audio in an Ogg or WebM container on all platforms.
• Theora video in an Ogg container on all platforms.
• VP8 video in a WebM container on all platforms.
• WAV audio on all platforms.

Opus, Vorbis, Theora and VP8 have the advantage of being open source and usable without paying license fees for generating and viewing content. Currently the decoding support in Firefox for these formats is not hardware accelerated. All decoding is done in software.

Support for the following formats in Firefox uses operating system decoder support. This means coverage is not available across all platforms. We are working towards this goal.

• H.264 video in an MP4 container on Firefox OS, some Android devices, and Desktop on Windows Vista and up.
• AAC audio in an MP4 container on Firefox OS, some Android devices, and Desktop on Windows Vista and up.
• MP3 audio in MP3 files on Firefox OS, some Android devices and Desktop on Windows Vista and up. Support for Windows XP is coming in Firefox 26.

These formats may use hardware accelerated decoding depending on operating system support. Support for these formats on other platforms is ongoing. On Linux we will use GStreamer. GStreamer playback support is already landed but not built by default. Enabling it is tracked in bug 886181. You can produce custom builds by using the configure switch --enable-gstreamer and setting the pref media.gstreamer.enabled to true.

Support for Mac OS X for H.264, AAC and MP3 is tracked by bugs 801521 and 851290.

Only a subset of Android devices are supported. For Android we are using libstagefright to provide hardware accelerated decoding. This uses an internal Android API that some device manufacturers customize which results in changes being needed to support specific devices. As a result we whitelist and blacklist devices that we know do or don't work. You can find the list of blacklisted or supported Android devices on the Mozilla wiki. Bug 860599 is a work in progress to implement a more reliable means of using libstagefright which should provide support on more devices.

All the formats listed above are what Mozilla has generally decided to support "on the web". That is, a web developer can expect to provide a video element with one of these formats as the source and expect it to play, if not now then at some point in the future.

There are some other formats that Firefox supports on specific operating systems or devices. These are primarily used in Firefox OS for system applications and to implement various mobile specifications. While supported on the device they are not guaranteed to be supported across all platforms or even on the web. They may only work on apps installed on the device. These formats are:

• 3GPP container on Firefox OS. This is used for MMS videos and video recording on the device.
• AMR audio format on Firefox OS. This is used for MMS and can only be played "on device" in privileged apps.

Other media formats may be supported in the future. VP9 and Daala for example are possibilities. For an official list of supported media formats, and the versions of Firefox they became supported, there is a supported media formats page on MDN. For discussion of formats and media in general there is the dev-media mailing list.

Progress Towards Media Source Extensions in Firefox

Update 2014-05-12: Matthew Gregan has a more recent post on Media Source Extensions support in Firefox Nightly.

There is a W3C editors draft for Media Source Extensions that provides a way for web applications to generate media streams for playback from JavaScript. This allows a number of new use cases on the web. A couple of examples might be:

• Media players that download encrypted content from a server, decode the data on the client using JavaScript, and send that data to the video player in a page.
• JavaScript implementations of adaptive streaming (for example, MPEG-DASH).

Work has been ongoing in Firefox to implement the specification. The majority of the work has been done by Matthew Gregan. The tracking bug for this is bug 778617. The dependancies of that bug list what needs to be implemented to complete support. Basic support is available in Firefox since bug 855130 landed.

That allows mediasource_demo.html to run in Firefox (that demo was originally from the URL mentioned in the bug report but hosted locally to have a stable source for testing).

The demo takes an existing VP8 encoded WebM file and splits it into five chunks, each chunk stored in a JavaScript typed array. The code looks like (reorganised from the demo for readability):

var mediaSource = new MediaSource();
var video = document.getElementById('video');
video.src = window.URL.createObjectURL(mediaSource);

var sourceBuffer = mediaSource.addSourceBuffer('video/webm; codecs="vorbis,vp8"');

var reader = new FileReader();
var file = new Blob([uInt8Array], {type: 'video/webm'});
var chunk = file.slice(startByte, startByte + chunkSize);

reader.onload = function(e) {
  sourceBuffer.appendBuffer(new Uint8Array(e.target.result));
  if (i == NUM_CHUNKS - 1) {
    mediaSource.endOfStream();
  }
}
reader.readAsArrayBuffer(chunk);

The createObjectUrl results in a blob URL that contains the media source data that is appended via source buffers. Playing the video using the standard HTML media API will result in it decoding and playing the binary data we've manually appended to the media source.

To run this demo you'll need to enable Media Source Extensions as it's currently switched off. Setting media.mediasource.enabled to true in about:config will turn it on. You'll want to use a nightly build to ensure you have the Media Source code and followup fixes.

Real world usage of Media Source extensions is more involved than that demo and there is much more to do. If you're interested in tracking progress you might like to track bug 778617. Support for a more advanced player is tracked in bug 881512. Completion of that bug should provide enough of the specification to run an MPEG-DASH Media Source demo where the MPEG-DASH code is implemented in JavaScript. This is one of the main goals at the moment.

Other browsers are also supporting Media Source Extensions. The MPEG-DASH demo currently runs in Chrome. The IE 11 preview implements MPEG-DASH support using Media Source Extensions. It'll be interesting to see what other uses web developers will find for this functionality once support becomes widely available.