Quick authentication using mobile devices and QR Codes

Isaac Potoczny-Jones

Introduction

In this blog post, we propose an authentication scheme using QR codes and Internet-connected smart phones to allow a user to quickly sign into a web site without having to memorize or type in a username and password. The user only has to prove that they are in possession of their mobile phone. We've developed a demonstration app and web site for this approach which you can try if you have an Android smartphone. Or you can watch the video demonstration. We have also started work on a draft REST protocol, and welcome feedback.

This work is preliminary, so we are very interested in feedback on the concept and prototype.

In general, authentication can be done using multiple “factors”. The more factors that are used, the more confidence a web site can have that they have truly identified the user:

• something a user knows, such as a password
• something the user has, such as a smart-card or cryptographic key
• something the user is, such as the user's fingerprint
• the user's location
• and probably many more

Many web sites currently use a single factor: a password. Our scheme can use a mobile phone as a second factor, or as a single factor: something the user has. In fact using a mobile phone as a single factor may be more convenient for the user and in some cases more secure than a password. One distinguishing feature of this approach is that it is not only a second factor but also a second channel. Unlike systems like Google Auth, the user does not input their second credential through their computer, but rather directly through the phone's network connection.

About QR Codes

QR codes are two dimensional bar codes that can contain a significant amount of information such as a shared key or session cookie. As in the following photograph, it is possible to disp lay a QR code on a computer screen and to scan that code with a mobile phone. This is an extremely common thing for Android users to do when they want to download apps that they have discovered on their computers. We utilize this capability to securely share secret information between the web site and the user.

User experience

In this scheme, there is a single step for both account creation and for subsequent log-in: The user scans a QR code. Edit: We have revised this workflow significantly. Please see the draft of the REST-based protocol.

Account creation: When a user visits a web site for the first time, the site generates and displays a QR code for login, and the user scans it. An account is created for them. They have no need to generate and record a username or password or any other information.

Log in: When a user subsequently visits a web site and needs to log in, the site displays a QR code that the user scans with the same mobile phone. The user is logged in without having to remember a username or password, or even remember whether they have visited that web site before.

The user can choose to increase security by locking their phone and encrypting its data. Since the web site and the phone can exchange complex data, a strong password can be generated and stored without the user having to memorize it.

In the following sections, we expand on this exchange by detailing the workflow, what is stored by each party, what attacks are mitigated, and what attacks are not mitigated.

Account creation workflow

1. The user visits a web site on their computer for the first time.
2. The web site generates and displays an Authentication Code (AC), which is a QR code.
   • The web site must generate a new session cookie to prevent against session fixation attacks.
   • The AC encodes the web site URL and a random secret. This will be the shared secret. (EDIT: There are trade-offs for this to become the shared secret, and that increases the trust in the QR code and the user's computer. In some circumstances, it may be better to have the app generate the shared secret.)
   • The random secret is tied to the session cookie stored in the computer's browser.
3. The user scans the Authentication Code with the “Animate Login App” (ALApp).
4. The ALApp decodes the AC and looks up the web site in the ALApp password table.
5. Since the web site is not in the ALApp password table, the ALApp creates a new entry and stores the random secret.(EDIT: Instead the App should generate a new random secret. This will become the shared secret.)
6. The ALApp also generates a random user identifier, or chooses a preferred username.
7. The ALApp uses the mobile phone's Internet connection to transmit the shared secret, the random secret, the session cookie, and the user identifier to the web site.
8. The web site verifies that the session cookie corresponds to the random secret. This random secret can only be used to authenticate this session cookie.
9. The web site creates an account for the user and adds the user identifier, along with the random secret to its user database.
10. The web site marks the session cookie as authenticated and redirects the browser into the authenticated portion of the web site.

User login workflow

1. The user visits a web site on their computer.

2. The web site generates and displays an Authentication Code (AC), session cookie, and random secret as above. (EDIT: Using both the session cookie and random secret is unnecessary. We have clarified this in the protocol draft.)

3. The user scans the Authorization Code with the Animate Login App (ALApp).

4. The ALApp decodes the AC and looks up the web site in its password table.

5. Since the web site already has an entry in ALApp password table, the ALApp looks up the shared secret and the user identifier.

6. The ALApp uses the mobile phone's Internet connection to transmit the random secret, the shared secret, and the user identifier to the web site.

7. The web site looks up the user identifier and verifies the shared secret.

8. The web site verifies that the session cookie corresponds to the random secret. This random secret can only be used to authenticate this session cookie.

9. The web site marks the session cookie as authenticated and redirects the browser into the authenticated portion of the web site.

Message format notes

• Since no one has to memorize the shared secret, it can be long and complex, protecting against brute-force attacks and simple guessing.
• The shared secret can be generated by the web site, and so follow that site's password complexity policy. However, if it's included in the QR code, then the code is much more sensitive.
• If the user's phone does not have a signal for an Internet connection, the user has a backup option of having the ALApp display the shared secret so the user can type it in.
• All messages must use HTTPS to authenticate the web site to the user and the smart phone.
• User identifiers can be random numbers and can be generated by the user or by the web site. Alternately, the user might set a preference on the ALApp for their favorite usernames, and the ALApp can negotiate with the web site to choose a username.
• User identifiers can be an email address.
• During account creation, the ALApp can be instructed to share or not share information with the web site depending on user preferences. For instance, the ALApp can share the user's email address, real name, photo, etc. On the other hand, the ALApp could only share a randomly generated username that can't be tied to user names on other web sites. Of course, some sites might require more information, and if so the user might decline to create an account on that web site.

Improving security with another factor

This scheme is most interesting (to us) as a single factor authentication for web sites which currently only use username and password combinations. This scheme makes logging into such sites quick and easy. However, this scheme can be used as a single factor or as a part of a multi-factor login. There are a variety of ways to add the second factor:

• The web site can maintain a username and password as before. The web site can enforce multi-factor authentication this way.
• The user can keep their phone locked, requiring a login password, unlock pattern (as on Android), or other method to unlock the phone. In this case, the user is accountable for deciding whether to use a second factor.
• Similarly, the user can store all of the shared secrets encrypted on their phone. They will need a master password to encrypt and decrypt these secrets, so the login process will be slightly slower, but they will still only have to memorize a single password. (EDIT: The newest version of the code in the git repository implements this.)
• Alternately, the user can choose which shared secrets they value most highly, and only encrypt those passwords, allowing them to log in to low-value web sites quickly, and higher-value web sites only by decrypting those passwords.

Attacks mitigated & other benefits

• Since the shared secret (the password) does not have to be memorized, or even typed in by a human, it can be long and complex. This mitigates against brute-force password crackers like John the Ripper (Peslyak, 2010) and Cain and Abel (Montoro, n.d.) both on the user's side and on the web site's side. This would prevent against attacks such as those used to crack so many users' passwords in the Gawker password database spill described in (Kennedy, 2010).
• Since the user does not type their password into the computer, a virus-installed keylogger or shoulder-surfer cannot capture their password.
• Similarly, the user can use an untrusted computer (such as one in an Internet cafe or hotel) without revealing their password.
• A phishing web site cannot capture the user password by tricking them into typing it in. The phone sends the shared secret, and will only send it to the web site in its database.
• Since the password is randomly generated, the user will not re-use passwords on different web sites, so a password crack on one web site will not lead to escalation of privileges on another, again as happened in the Gawker password database spill (Pompeo, 2010).
• If the user chooses to use a randomly generated username, the user's account on one web site cannot be associated with the user's account on another web site, again as happened in the Gawker password database spill.
• Users have more privacy options since it is easier to generate and recall random passwords.
• The user will not lose access to a web site because they cannot remember a password.
• Since the authentication code is sent encrypted, and the web site authenticates itself to the user via HTTPS, the random secret can't be intercepted to authenticate another user's session.
• In several respects, this approach is similar to a browser storing passwords on behalf of a user. The major advantage this approach has is that one can easily move identities between machines.
• Finally, the login process is quicker and easier than typing a username and password.

Vulnerabilities

• This scheme does not prevent man-in-the-middle attacks; these need to be mitigated by HTTPS.
• Edit: A vulnerability pointed out by Michael Tschannen is a variant of session fixation that requires a phishing attack. An attacker generates an AC for a target site and therefore knows the session cookie. The attacker tricks a user into visiting a less-trusted site and trying to log into that site. The attacker puts the AC for the target site into the (fake) less-trusted site. The user scans the AC, authenticating the attacker to the target site. This can be mitigated in two ways: 1) require that the user select the site they are logging into on the ALApp, or 2) confirm with the user the site they are logging into before sending the shared secret.
• If the phone is lost or damaged, the user cannot access their web sites. This can be mitigated by storing the user's email address for password reset or authorizing a new phone. Another option is to encrypt the phone's password database and store it in the cloud or otherwise backing it up.
• If the phone is stolen, the attacker can impersonate the user; therefore it is most likely desirable to encrypt the shared secrets on the phone and to authenticate the user to the phone with a single password, as above. This may not be necessary for web sites that are of low value to the user.
• If the phone is stolen, it may be desirable to issue a revocation of all related passwords at once, rather than individually logging into different web sites.
• When using an untrusted computer (one with a virus or in a hotel lobby), the user's account is still vulnerable as long as the session is active.
• Many of these vulnerabilities are equivalent to any system which stores a user's passwords on their phone.

Related authentication systems

• The ALApp can be integrated with an InfoCard / CardSpace client on the phone.
• As with any authentication mechanism, this can be used to authenticate to an OpenID provider.
• The workflow can be modified to use a Public Key Infrastructure instead of shared secrets. This might allow smoother revocation by issuing a revocation certificate if the phone is stolen.

Demonstration system notes

We have implemented a demonstration system which you can try out to experiment with this method of logging in. It has a number of limitations, the most obvious of which is that it can only be used to log into the demonstration web site; it will only remember one username and password. We implemented the web site login by creating a Drupal module in the hopes that it will eventually be possible to allow this type of login by installing the module. Not all of the features discussed in this paper are in the current module version. Our plan is to release the module and the app open source.

One attractive feature of this scheme is that web sites don't have to move away from using cookies, usernames, and passwords so their back-end functionality does not have to change, only the login process.

Zebra Crossing (ZXing) is a QR-code reader on Android that can easily be integrated with other apps such as ALApp.

OI Safe is an encrypted password store on Android that has an API allowing other authorized apps, such as the ALApp, to store and retrieve passwords (Potoczny-Jones, 2009).

Related work

There is a lot of work in using mobile phones as a factor in authentication. Google web applications can be configured to use a second factor, either an app installed on a phone, or a text message sent to a phone (Feigenbaum, 2010). In each case, the user is presented with a code that they type into the web site. Our proposed scheme does not require the user to type anything into the web site. It also uses a separate channel, and so mitigates "man in the browser" attacks to some extent.

Liao & Lee (2010) propose a QR-code authentication system for generating one-time passwords. Their system is more complex since it provides for mutual authentication (we use HTTPS) and yet still requires some secure channel between the web site and the mobile app.

Safelayer describes a similar authentication system using asymmetric encryption (Safelayer, n.d.). However, this is described as a multi-factor system, and requires web sites to modify their back-end systems to use public/private keypairs. Our proposed system still uses simple username / password combinations.

A system for authenticating transactions on untrusted terminals using QR codes is described in (Starnberger, Froihofer, and Goeschka, 2009) but also uses PKI and requires the user to enter a code into the computer after the smart phone performs a computation.

Conclusion

We are seeking feedback on this approach. If you see any security issues, please inform us. EDIT: We have received a lot of good feedback. There was a good discussion on Reddit's netsec that was mostly positive.

We have outlined a scheme whereby a mobile phone can be used as an authentication mechanism using QR codes. This scheme could allow users to log into a web site using a single step: scanning a QR code from their mobile phones. Alternately, this scheme can be used as one factor in multi-factor authentication.

QR codes, mutli-factor authentication, and Internet-connected smart-phones are “in the air” and others have likely come up with similar schemes. We have written this paper because we haven't found any other description of such a system, nor seen one in the wild. Mostly, we would like to use such a system since it would improve security and convenience on the Internet, so please implement this and release it open source, or help us to do so :-)

References

Feigenbaum, E. (2010). A more secure cloud for millions of Google Apps users. Official Google enterprise blog. Retrieved from http://googleenterprise.blogspot.com/2010/09/more-secure-cloud-for-millions-of.html

Kennedy, D. (2010). The real lessons of Gawker's security mess, The Firewall. Forbes. Retrieved from http://blogs.forbes.com/firewall/2010/12/13/the-lessons-of-gawkers-security-mess/

Liao, K., & Lee, W. (2010). A Novel User Authentication Scheme Based on QR-Code . Journal of networks, vol. 5, no. 8. Retrieved from http://www.academypublisher.com/ojs/index.php/jnw/article/viewFile/0508937941/2055

Montoro, M. (n.d.). Cain & Abel user manual. Retrieved from http://www.oxid.it/ca_um/

Peslyak, A. (2010). John the Ripper user manual. Retrieved from http://www.openwall.com/john/doc/CREDITS.shtml

Pompeo, J. (2010). Leaked Gawker passwords cause trouble on GMail, Twitter [web log post]. Retrieved from http://news.yahoo.com/s/yblog_thecutline/20101213/bs_yblog_thecutline/leaked-gawker-passwords-cause-problems-on-twitter-gmail

Potoczny-Jones, I. (2009). CryptoIntents, A discussion of the cryptography and keystore intents in OI Safe. Retrieved from https://code.google.com/p/openintents/wiki/CryptoIntents

Safelayer. (n.d.) QR-Scan OTP: ergonomic authentication. Retrieved from http://sandbox.safelayer.com/index.php?option=com_content&view=article&id=466%3Aqr-scan-otp-ergonomic-authentication&catid=1%3Asemantic-web-trust-portal&Itemid=2&lang=en

Starnberger G., Froihofer L., and Goeschka, K. M. (2009) . QR-TAN: Secure Mobile Transaction Authentication . IEEE Computer Society. Retrieved from http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.149.2315&rep=rep1&type=pdf

cabal-dev: sandboxed development builds for Haskell

Performing consistent builds is critical in software development, but the current system in GHC/Haskell of per-user and per-system GHC package databases interferes with this need for consistency. It is difficult to precisely identify the dependencies of a given project, and changes necessary to enable one project to build may render another project inoperable. If each project had a separate package database, each project could be built in a sandbox.

Galois has released cabal-dev:  a tool for managing development builds of Haskell projects within sandboxes.

Both cabal-install repositories and sandboxed ghc package databases are used to prevent interactions between disparate projects, or user package databases. cabal-dev is similar to capri, which was coincidentally developed concurrently. The two projects take slightly different approaches to sandboxing, and exhibit slightly different behaviors depending on the state of the global package database, and the versions of the tools installed.

For most packages, just use cabal-dev instead of cabal, and you will get a sandboxed build that will not install anything (even automatically installed dependencies) into the user or global ghc package databases. If your build depends on patched or unreleased libraries, you can add them to your sandboxed build environment so they can be installed by cabal-dev or cabal by running:

> cabal-dev add-source /path/to/source/code

Where /path/to/source/code is either a path to a source directory containing a .cabal file, or an sdist tarball.Cabal-dev has been in use at Galois for roughly six months now, but it should currently be treated as alpha software: we've exercised a few execution paths heavily, but it still has a number of rough edges.Cabal-dev is hosted on hackage and git-hub. A brief tutorial can be found in the README.md.

Galois releases the Haskell Lightweight Virtual Machine (HaLVM)

Galois, Inc. is pleased to announce the immediate release of the Haskell Lightweight Virtual Machine (or HaLVM), version 1.0. The HaLVM is a port of the GHC runtime system to the Xen hypervisor, allowing programmers to create Haskell programs that run directly on Xen’s “bare metal.” Internally, Galois has used this system in several projects with much success, and we hope y’all will have an equally great time with it.

What might you do with a HaLVM? Pretty much anything you want. :) Explore designs for operating system decomposition, examine new notions of mobile computation with the HaLVM and Xen migration, or find interesting network services and lock them inside small, cheap, single-purpose VMs.

The HaLVM is the result of many years of effort, by many people inside Galois.  Although it is not yet totally bug-free, we have decided that broad adoption wins over perfection and thus we are releasing it for general review. As such, there will be some rough edges, and we urge you to read the documentation to understand the platforms we test on.

We are releasing the HaLVM under a non-restrictive BSD3 license. You can find it here:

http://halvm.org

We welcome user feedback, feature requests, bug notices, patches, and feature additions; see the page above for guidelines on getting involved.

Finally, we’d like to give many things to the GHC and Xen communities, without which this work would not be possible.

If you have any questions or concerns, please don’t hesitate to contact the HaLVM’s maintainers at halvm-devel@community.galois.com.

Have a lovely day!

Tech Talk: The Rubinius Virtual Machine

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:

The Rubinius Virtual Machine

speaker:

Brian Ford

time:

10:30am, Tuesday, 30 November 2010

location:

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:

Ruby is a highly dynamic, strongly-typed programming language created by Yukihiro Matsumoto in 1993 and first released in 1995. It borrows from Smalltalk, Lisp, and Perl. Ruby has single inheritance, mixins, and syntax features like omission of parentheses that make it well-suited for embedded domain-specific languages. Ruby was popularized by the Ruby on Rails web development framework.The Rubinius project began as an implementation of the Ruby programming language roughly following the design of the Smalltalk-80 virtual machine described in the Blue book ("Smalltalk-80: the language and its implementation" by Adele Goldberg and David Robson). We have extended the initial implementation based on modern research in virtual machines, garbage collectors, and just-in-time (JIT) compilers. Rubinius currently features a stack-oriented opcode virtual machine, generational garbage collector, and LLVM-based JIT compiler. Most of the Ruby core library and the bytecode compiler are written in Ruby.We will examine the main features of Rubinius and take a deeper dive into some aspects of the virtual machine and JIT compiler. We will also look at possible future work to address memory load, startup, and suitability for using Rubinius in Android phones. If there is time and interest, we will discuss implementing programming languages besides Ruby on Rubinius.

bio:

Brian Ford began contributing to the Rubinius project in December 2006 shortly after the creator, Evan Phoenix, announced the project. He is presently employed by Engine Yard, Inc to work full-time on Rubinius. Brian is keenly interested in languages of all kinds, from mathematics and various programming languages to Spanish and Japanese. He has primarily used C/C++, Tcl, Python, and Ruby in Geographic Information Systems, physical security systems monitoring and web application development. He has a B.Sc. in Mathematics from Portland State University.

Click to read more ...

Copilot: a DSL for Monitoring Embedded Systems

Introducing Copilot

Can you write a list in Haskell? Then you can write embedded C code using Copilot. Here's a Copilot program that computes the Fibonacci sequence (over Word 64s) and tests for even a numbers:

fib :: Streamsfib = do"fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")"t" .= even (var "fib")where even :: Spec Word64 -> Spec Booleven w = w `mod` const 2 == const 0

Copilot contains an interpreter, a compiler, and uses a model-checker to check the correctness of your program. The compiler generates constant time and constant space C code via Tom Hawkin's Atom Language (thanks Tom!). Copilot is specifically developed to write embedded software monitors for more complex embedded systems, but it can be used to develop a variety of functional-style embedded code.Executing

> compile fib "fib" baseOpts

generates fib.c and fib.h (with a main() for simulation---other options change that). We can then run

> interpret fib 100 baseOpts

to check that the Copilot program does what we expect. Finally, if we have CBMC installed, we can run

> verify "fib.c"

to prove a bunch of memory safety properties of the generated program.Galois has open-sourced Copilot (BSD3 licence).  More information is available on the Copilot homepage.  Of course, it's available from Hackage, too.

Flight of the Navigator

Copilot took its maiden flight in August 2010 in Smithfield, Virginia. NASA rents a private airfield for test flights like this, but you have to get past the intimidating sign posted upon entering the airfield. However, once you arrive, there's a beautiful view of the James River.We were flying on a RC aircraft that NASA Langley uses to conduct a variety of Integrated Vehicle Health Management (IVHM) experiments. (It coincidentally had Galois colors!)  Our experiments for Copilot were to determine its effectiveness at detecting faults in embedded guidance, navigation, and control software.  The test-bed we flew was a partially fault-tolerant pitot tube (air pressure) sensor.  Our pitot tube sat at the edge of the wing.  Pitot tubes are used on commercial aircraft and they're a big deal: a number of aircraft accidents and mishaps have been due, in part, to pitot tube failures.Our experiment consisted of a beautiful hardware stack, crafted by Sebastian Niller of the Technische Universität Ilmenau.  Sebastian also led the programming for the stack.  The stack consisted of four STM32 ARM Cortex M3 microprocessors.  In addition, there was an SD card for writing flight data, and power management. The stack just fit into the hull of the aircraft. Sebastian installed our stack in front of another stack used by NASA on the same flights.The microprocessors were arranged to provide Byzantine fault-tolerance on the sensor values.  One microprocessor acted as the general, receiving inputs from the pitot tube and distributing those values to the other microprocessors.  The other microprocessors would exchange their values and perform a fault-tolerant vote on them.  Granted, the fault-tolerance was for demonstration purposes only: all the microprocessors ran off the same clock, and the sensor wasn't replicated (we're currently working on a fully fault-tolerant system). During the flight tests, we injected (in software) faults by having intermittently incorrect sensor values distributed to various nodes.The pitot sensor system (including the fault-tolerance code) is a hard real-time system, meaning events have to happen at predefined deadlines. We wrote it in a combination of Tom Hawkin's Atom, a Haskell DSL that generates C, and C directly.Integrated with the pitot sensor system are Copilot-generated monitors. The monitors detected

• unexpected sensor values (e.g., the delta change is too extreme),
• the correctness of the voting algorithm (we used Boyer-Moore majority voting, which returns the majority only if one exists; our monitor checked whether a majority indeed exists), and
• whether the majority votes agreed.

The monitors integrated with the sensor system without disrupting its real-time behavior.We gathered data on six flights.  In between flights, we'd get the data from the SD card.We took some time to pose with the aircraft. The Copilot team from left to right is Alwyn Goodloe, National Institute of Aerospace; Lee Pike, Galois, Inc.; Robin Morisset, École Normale Supérieure; and Sebastian Niller, Technische Universität Ilmenau. Robin and Sebastian are Visiting Scholars at the NIA for the project. Thanks for all the hard work!There were a bunch of folks involved in the flight test that day, and we got a group photo with everyone. We are very thankful that the researchers at NASA were gracious enough to give us their time and resources to fly our experiments. Thank you!Finally, here are two short videos. The first is of our aircraft's takeoff during one of the flights. Interestingly, it has an electric engine to reduce the engine vibration's effects on experiments.

Untitled from Galois Video on Vimeo.

The second is of AirStar, which we weren't involved in, but that also flew the same day. AirStar is a scaled-down jet (yes, jet) aircraft that was really loud and really fast. I'm posting its takeoff, since it's just so cool. That thing was a rocket!

Untitled from Galois Video on Vimeo.

More Details

Copilot and the flight test is part of a NASA-sponsored project (NASA press-release) led by Lee Pike at Galois.  It's a 3 year project, and we're currently in the second year.

Even More Details

Besides the language and flight test, we've written a few papers:

• Lee Pike, Alwyn Goodloe, Robin Morisset, and Sebastian Niller. Copilot: A Hard Real-Time Runtime Monitor. To appear in the proceedings of the 1st Intl. Conference on Runtime Verification (RV'2010), 2010. Springer.

This paper describes the Copilot language.

• Lee Pike. Schrödinger's CRCs (Fast Abstract). 40th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2010), 2010.

Byzantine faults are fascinating.  Here's a 2-page paper that shows one reason why.

• Alwyn Goodloe and Lee Pike. Monitoring distributed real-time systems: a survey and future directions. NASA Contractor Report NASA/CR-2010-216724, 2010.

At the beginning of our work, we tried to survey prior results in the field and discuss the constraints of the problem.  This report is a bit lengthy (almost 50 pages), but it's a gentle introduction to our problem space.

• Lee Pike, Geoffrey M. Brown, and Alwyn Goodloe. Roll your own test bed for embedded real-time protocols: a Haskell experience. In Haskell Symposium, 2009.

Yes, QuickCheck can be used to test low-level protocols.

• Alwyn Goodloe and Lee Pike. Toward monitoring fault-tolerant embedded systems (extended abstract). In International Workshop on Software Health Management (SHM'09), 2009.

A short paper motivating the need for runtime monitoring of critical embedded systems.

You're Still Interested?

We're always looking for collaborators, users, and we may need 1-2 visiting scholars interested in embedded systems & Haskell next summer.  If any of these interest you, drop Lee Pike a note (hint: if you read any of the papers or download Copilot, you can find my email).

Click to read more ...