On my recent trip to Arizona for CCS 2014 I took some time out to fly paragliders in the desert with Arizona Paragliding. Turns out that they also design and manufacture the SlingMachine towing winch that is used to transport paraglider pilots safely the desert floor to 3,000 feet in a matter of minutes. When I arrived Sean Buckner the designer and creator of SlingMachine was in the process of automating the towing winch. Sean had already designed and built the electronics for the automated control system on the SlingMachine and I helped design and build the software for the automated control box.

This is me being towed to into the air by the SlingMachine controlled by software designed and written by myself and Sean Buckner:

It felt amazing to be towed into the air by my own software and when we perfected the software I could to actually feel changes we were making to the software.

This is very cool but you may be wondering how is this relevant to software reliability and security; the end goal of the project is to develop embedded devices (hardware and software) that put some science into improving the safety of paragliding as a sport.

We have made a start by creating an automated control box (with associated software) for the SlingMachines winch. The automated control box makes the towing process more repeatable (delivering the same tow every time) and thereby safer because it is less prone to certain categories of operator error. We are also developing a pilot telemetry pack to increase pilot safety on the towing line and a novice pilot telemetry pack to help with pilot safety during training flights.

This blog entry about what I feel is a cool software project with obvious safety and reliability issues. It is also a call for help, to the members of the Secure and Reliant Systems (SRS) and Centre for Software Reliability (CSR), we are continuing to develop the software and create new projects that are designed to improve safety in paragliding.

So my question to you guys, is how do we development ultra-reliable software, quickly with minimal manpower?

What does the software do?

The software we wrote controls the winch towing the paraglider pilot into the air, and as the pilot on the end of the tow line you want to know that the software is going to perform reliably and not do anything unexpected.

We only had a short time to implement the software and very limited manpower, this creates a problem as high integrity software development techniques significantly increase the development time / manpower required. So we had to get smart to develop highly reliable software in a rapid application development (RAD) scenario. To achieve this we applied these six principles:

1. Human operator override; this is an essential safety feature in our approach to developing and testing the software. The human tow operator can, at any point, flick a switch to override the software and take control of the towing process. Just like the pilot on modern jet liner who has the ability to override the autopilot when the situation exceeds the conditions the autopilot can deal with. In both systems the human is the final safety backstop.
2. Keep it simple; don’t over complicate the software.
3. Build test environment for the control box; this consisted of a set of potentiometers and switches that replicated the inputs of the sensors on the SlingMachine winch. We could set the dials to replicate any given situation on a tow without actually launching a glider.
4. Split the software into small self contained functional elements, each of which can be implemented and tested separately. We would complete each element and lock it off before moving onto the next.
5. Test, test and test again… structured edge case testing allows us to repeatedly test situations that may only occur once in a thousand tows. This means that when that 1 in 1,000 case occurs the software will handle it.
   To achieve this we built a static test environment for the control box, which mimicked the input from the sensors on the towing winch using potentiometers and switches. The test environment allows us to set up those 1 in 1000 scenarios on the bench rather than in the field.
6. Good old fashioned debug text output; the Arduino micro controller, on which the software was built, can output a constant stream of debug text over the serial line to a PC which records the data. This gives us a text log of each line of code the Arduino runs. We can then analyse the test log after each test run to verify that the software operated as expected given the inputs from the tow operator and the pressures exerted on the tow line by the glider pilot.

Our strategy delivered ultra reliable software in a very short time with minimal manpower resources. However this does pose a very important the question; was the quality of the software we produced improved by the fact that we were flying the test flights towed by our own software?

Software Design

The physical design of the SlingMachine is based on a variable friction tow line pay out systems. This design means that when the glider exerts more force on the tow line the winch will increase the rate at which the tow line is released thereby smoothing out towing experience for the paraglider pilot.

In addition the skill and experience of the towing operators Sean and Abe Heward ensures a safe and smooth ride to 3,000 feet every time.

So what does the software automate?

To automate the towing process we needed to capture the knowledge inside the head of SilngMachine’s creator/designer Sean and condense that into software. The objective being to create software that can deliver as safe and reliable a tow as the human operator.
By no means does the software replace the tow operator, as the operator is performing the complex task of monitoring the flight of the pilot and glider to ensure that they are flying safely. The software takes over the monitoring the towing pressure exerted on the glider and adjusting the towing speed to compensate for changes in the wind speed / direction and the effect of thermals.

This allows the tow operator to concentrate on how the pilot is flying; focussing on whether to proceed with the tow or to abort the tow if the pilot gets into difficulties. For instance, during the launch phase while the pilot is running along the ground, verifying that the paraglider wing is flying straight and level above the pilot’s head before applying the additional tow pressure to lift the pilot into the air.

So why is the towing pressure exerted on the pilot important?

Because the air is lumpy; ultra-light aircraft, such as paragliders and hang gliders, are very sensitive to wind gusts, wind shifts and to rising/descending air caused by thermals. The air through which the glider is travelling can change speed and direction relative to the towing force, which is attached to the ground. This causes the force excreted on the glider to change rapidly even though the speed of the towing vehicle and the force applied by the towing winch remain the same.

These two photos show a whiteboard design session where we are discussing the a mild feedback oscillation created when the pilot has several hundred feet of altitude, meaning that there is several hundred feet of tow line between the pilot and the towing winch. The control box detects a change in force exerted on the tow line and alters the towing pressure accordingly, however there is a delay between the change in towing resistance and the resultant effect on the glider. The control box must compensate for this delay otherwise it causes a feedback oscillation, which the pilot feels as a gentle pull and relax, pull and relax motion. What was really cool for me was being the pilot on the end of the tow line, feeling that oscillation and knowing exactly what the software was doing and why. Thinking to myself when I get back on the ground I know how to fix that.

Whiteboard session 1

Whiteboard session 2

The SlingMachine control box

The control box has 2 dials to set (1) the target towing resistance based on the pilot weight (2) the target towing force adjusting for wind shifts and thermals experienced by the glider. There are 5 mode switches for the different stages of the tow:

Pre-tension;
Puts tension on the towing line prior to launch

Pre-launch;
Increases the line tension assisting the pilot whilst transitioning from pilot stationary and glider on the ground to pilot running on the ground with the glider flying above his/her head
Launch; once the glider is flying straight and stable, increase the line tension to lift the pilot into the air and gain some initial altitude

Towing;
This is the main body of the tow when the pilot will gain the majority of the altitude

Rewind;
When the tow is complete and the pilot releases the towline the winch automatically rewinds the towing line.

The control box is based on the Arduino Mega 2560 micro controller, which is perfect for the task of constantly monitoring several analogue input channels and setting the appropriate outputs to control devices in the physical world.

What lessons did I learn?

Developing this software was the most fun and the biggest challenge.
We developed highly reliable software in a short space of time with minimal resources, however in my view this was only possible on a small scale project such as the SlingMachine towing software. This is because the software is performing a relatively simple and well defined set of tasks; the software monitors the towing pressure applied to the pilot and adjusting it to maintain the optimum in changeable flight conditions.
The five principles we used to develop the software focused on creating ultra reliable software with the limited resources at our disposal. The principles were based on common sense and 25+ years of developing high integrity systems.

Given my background in high integrity systems the next step for the SlingMachine software is to run extensive edge case testing on the software. To this end we have built a test rig for the control box, with which we can feed in sensors readings as if they came from the SlingMachine winch. The sensor readings can come from 2 sources:

1. We can dial in sensor readings with potentiometers. This allows us to test the edge cases that may only occur in 1 in 1,000 tows.
2. We can playback real input sensor readings recorded from actual tows of real pilots. These recordings allow us refine the software algorithms comparing the performance of the new software revisions against the recording of the old software. The advantage of using recorded sensor readings to test the software is that the tests are as close to real life as possible without a real pilot having to leave the ground.

So What Next?

The initial software development was done in 3 weeks, which was the duration of my visit to Arizona, during which the primary aim was to get the software operational before the end of my trip. We are now developing new embedded hardware / software modules to monitor live telemetry from the pilot and further enhance pilot safety.

Tow pilot telemetry pack:
Which monitors the flight of the paraglider pilot and relays that information to the tow operator at the controls of the winch. This gives the tow operator much better picture of whether the pilot is flying well or if things are starting to go outside the norm. This is especially valid when the pilot has gained some altitude and so is further away and the visual signs that the pilot is getting into difficulties are much harder to see.

Novice pilot telemetry logging pack;
Once a novice pilot has released from the tow line they are in free flight under the instruction (over the radio) from an instructor on the ground. The novice pilot has a number of tasks to do on each of their free flights and these tasks would usually be done at the highest possible altitude as this gives the greatest safety margin when trying new manoeuvres. The recorded telemetry allows the instructor to better understand what the pilot did during their flight – pilot position, height, turning forces, rate of climb / decent and lateral acceleration.
This data also allows the instructor to verify that the novice pilot has completed the assigned task when the pilot might be at several thousand feet when the task is performed. It may also be the case that glider has done something the novice pilot did not expect during the flight, either because of external forces (wind or thermals) or because of the over active input from the pilot, instructor can also use the telemetry data to help the novice understand what happened and what to do in the future.

Novice pilot safety pack;
This will be an extension to the novice telemetry pack which will use the input from the sensors such as the accelerometer and barometric altimeter to identify when the pilot gets into unsafe situations. For instance sounding a warning if the pilot performs aggressive turns at low an altitude or if the pilot is performing an increasingly aggressive spiral turn greater than 3600
The development strategy we have used so fare for the development of the SlingMachines control box has worked well so far. We are very open to suggestions for a development strategy that will enhance the security and reliability of pilot safety projects and the continuing development of the control box as we move forward in the development and the software gets more complex.

Thanks,

Martin Emms

Aad raises a good question in his blog post; Why are we using reliability / dependability tools and techniques such as Praxis methodology and Z modelling to identify flaws in the existing EMV payment system?  These tools were intended to be used to in the building of reliable systems, however we are using them to analyse the security / reliability of an existing system post implementation.

Our CCS 2014 paper “Harvesting High Value Foreign Currency Transactions from EMV Contactless Credit Cards without the PIN” outlines the methodology we have developed for analysing the EMV payments protocol.  The methodology uses (i) abstract modelling to identify potential anomalies in the EMV payments protocol (ii) software emulation to exhaustively test real-world implications of the anomaly on credit/debit cards (iii) practical demonstrations of any flaws identified, allowing us to better communicate our findings to the general public and the banks.

In short the methodology we have developed is the scientific contribution that underpins our work, without which it could be argued that we were simply lucky hackers who have stumbled across some interesting bugs in the EMV implementation.

So far the methodology has identified the Foreign Currency flaw (CCS 2014) and the Contactless PIN Verify flaw (FC 2013) both of which stem from the specification NOT detailing what should happen under a given set of circumstances.  This is where we get back to Aad’s question “Why are we using reliability tools for our analysis?”; Leo Freitas’s abstract model is very good at identifying conditional cases that are not satisfied by the specification, highlighting a missing case (which is not handled) rather than an incorrect case or an exception case, something we human are quite bad at seeing.

The system designers and coders are usually focused on making the system work and dealing with the expected exception cases; this is perfectly valid as this is the most efficient route to delivering a working system.  However this may lead to the assumption that a particular set of exception values would not occur together and therefore the exception case is not handled.  This un-handled case shows up as an anomaly in Leo’s abstract model => which leads to testing in the EMV emulator => which leads to a practical demonstration of the flaw=> which leads to a paper at CCS => and eventually ends up on the BBC News.

This year I have found it a little frustrating that the sensational “hack” papers grab the headlines and are easiest to get published at a good conference (we also wrote a “solution” paper and a “methodology” paper this year which generated zero interest and were not published).  However what we learned from the CCS paper reviews was that the best paper combines all 3 elements; good science in the “methodology”, good results in the “hack” and a responsible set of possible “solutions” in the conclusion.

Hopefully my random ramblings have been of some help

Slides from CCS 2014 presentation CCS2014_foreign-currency_v1-2

At various presentations and also in our research on credit cards I came across approaches for security vulnerability research that are based on tools and techniques for building reliable systems.  I am curious about the relation between the two, and thought maybe a blog is a good venue for people to share some thoughts on the issue.

A couple of examples of what I mean:

– Martin is trying to build a reliable emulator for credit card payment. He works with Leo on proofs for reliability. Martin essentially follows the Praxis software development approach, in a light-weight incarnation. But, as a consequence, he and Leo find security vulnerabilities. Shouldn’t we have used a tool/method that aims at finding security vulnerabilities instead of one that aims at building reliable systems?  Or are these somehow the same?

– We recently had a colloquium guest speaker (recently graduated PhD student) from Glasgow who talked about her research in using safety case description languages to describe case studies for security breaches.  Such use is almost contrary to what the language was defined for, but it seemed to work.

I’m interested in the question whether we use existing dependability/safety techniques for security research because (1) we don’t have better ones yet or because (2) they are the best ones imaginable.  I guess the answer is ‘it depends’, but it struck me as interesting to try to understand this issues more generically and discuss on this blog.  So, please comment.

In a forthcoming paper (to be presented at SSR’14), we (with Siamak Shahandashti) present some new attacks on SPEKE, an internationally standardized protocol. The idea originated from a causal chat over coffee with my colleague, Siamak Shahandashti, four days before the SSR’14 submission deadline. But the idea was interesting enough (to us) that we decided to write a paper. It was intensive a few days’ work, but it turned out to an enjoyable experience. A preprint of the paper can be found here (also in the IACR ePrint).

Background: SPEKE is one of the most well-known Password Authentication Key Exchange (PAKE) techniques. It was first designed in 1996 by David Jablon. Over the past twenty years, it seems to have withstood various attacks, and yet no major flaws has been found. To date, the SPEKE protocol has been included into the IEEE P1363.2 and ISO/IEC 11770-4 standards, and deployed in commercial products (for example, Blackberry).

Our findings: However, in our paper, we identity two weaknesses in SPEKE, which seem to have evaded previous efforts of cryptanalysis. First, we show an impersonation attack, in which an attacker is able to impersonate a user by engaging in two parallel sessions with the victim. Second, we show a key-malleability attack, in which a man-in-the-middle attacker is able to manipulate the session key established between two honest users without being detected. We further explain the applicability of the attack to the SPEKE variants defined in IEEE P1363.2 and ISO/IEC 11770-4 and point out deficiencies in both standards.

Suggested changes to standards:  Finally, we propose concrete changes to both the IEEE and ISO/IEC standards. The changes that we propose not only address all currently known attacks against SPEKE, but also improve the round efficiency of SPEKE as it is currently defined in the standards.

For more technical details, please refer to our paper. Any comments are of course most welcome.

Updates:

• 2014-10-24: during the ISO/IEC JTC 1/SC 27 Meeting held in Mexico (19-24 Oct, 2014), it has been agreed by the national bodies present in the meeting to revise the SPEKE specification in ISO/IEC 11770-4 to address the two attacks reported in our SSR’14 paper.

While the original idea could be traced back to a chapter in my PhD thesis, the actual work on large-scale e-voting started in 2009 when I was still working in Cambridge. With my colleague Matthew Kreeger, we began to critically examine the basic theory underpinning the 20 years research on End-to-End (E2E) verifiable e-voting, and attempted to design a new category of E2E systems that did not rely on any trustworthy tallying authorities. We called the new category “self-enforcing e-voting”.

We first released a technical report in IACR (2010), and then tried to publish it at a conference.

http://eprint.iacr.org/2010/452

Until its recent acceptance by USENIX JETS (Vol. 2, No. 3, 2014), the paper had been repeatedly rejected by top conferences in the field. The final version of the paper is in the open-access domain (below). The technical protocol in the paper remains unchanged from its 2010 IACR report.

https://www.usenix.org/jets/issues/0203/hao

This has been an interesting personal experience, from receiving consistently harsh reviews and repeated rejections from top conferences, to getting surprisingly positive feedback from the ERC panel and a €1.5m starting grant to support my further work, until the final acceptance of the paper just recently.

Getting rejections is always a frustrating experience, but in the end, I feel I learned most from the rejections rather than the acceptance. Today’s top security conferences have developed an extremely rigorous reviewing process, which is good. But perhaps, the process could be slightly adjusted to give a little bit more tolerance to “new” ideas, albeit they may be controversial or have all sorts of shortcomings in the beginning.

Acknowledgement: The co-authors of the paper are Matthew Kreeger, Brian Randell, Dylan Clarke, Siamak Shahandashti and Peter Lee. We especially thank several dozens of anonymous reviewers – who liked or disliked the paper – for the feedback and for helping us improve the paper.