Showing posts with label safety-critical systems. Show all posts
Showing posts with label safety-critical systems. Show all posts

Thursday, 10 October 2019

If the world was a (temporal) database...

I thought I might share a problem we've been discussing in my Cornell PhD-level class on programming at the IoT edge.

Imagine that at some point in the future, a company buys into the idea (my idea!) that we'll really need smart highway systems to ever safely use self-driving cars. A bit like air traffic control, but scaled up.

In fact a smart highway might even offer guidance and special services to "good drivers", such as permission to drive at 85mph in a special lane for self-guided cars and superior drivers... for a fee.  Between the smart cars and the good drivers, there would be a lot of ways to earn revenue here.  And we could even make some kind of dent in the endless gridlock that one sees in places like Silicon Valley from around 6:45am until around 7pm.

So this company, call it Smart Highways Inc, sets out to create the Linux of smart highways: a new form of operating system that the operator of the highway could license to control their infrastructure.

What would it take to make a highway intelligent?  It seems to me that we would basically need to deploy a great many sensors, presumably in a pattern intendent to give us some degree of redundancy for fault-tolerance, covering such things as roadway conditions, weather, vehicles on the road, and so forth.

For each vehicle we would want to know various things about it: when it entered the system (for eventual tolls, which will be the way all of this pays for itself), its current trajectory (a path through space-time annotated with speeds and changes in speed or direction), information about the vehicle itself (is it smart?  is the driver subscribed to highway guidance or driving autonomously?), and so forth.

Now we could describe a representative "app": perhaps, for the stretch of CA 101 from San Francisco to San Jose, a decision has been made to document the "worst drivers" over a one month period.  (Another revenue opportunity: this data could definitely be sold to insurance companies!)   How might we do this?  And in particular, how might we really implement our solution?

What I like about this question is that it casts light on exactly the form of Edge IoT I've been excited about.  On the one hand, there is an AI/ML aspect: automated guidance to the vehicles by the highway, and in this example, an automated judgement about the quality of driving.  One would imagine that we train an expert system to take trajectories as input and output a quality metric: a driver swerving between other cars at high speed, accelerating and turning abruptly, braking abruptly, etc: all the hallmarks of poor driving!

But if you think more about this you'll quickly realize that to judge quality of driving you need a bit more information.  A driver who swerves in front of another car with inches to spare, passes when there are oncoming vehicles, causes others to break or swerve to avoid collisions -- that driver is far more of a hazard than a driver who swerves suddenly to avoid a pothole or some other form of debris, or one who accelerates only while passing, and passes only when nobody is anywhere nearby in the passing lane.  A driver who stays the right "when possible" is generally considered to be a better driver than one who lingers in the left, if the highway isn't overly crowded.

A judgment is needed: was this abrupt action valid, or inappropriate?  Was it good driving that evaded a problem, or reckless driving that nearly caused an accident?

So in this you can see that our expert system will need expert context information.  We would want to compute the set of cars near each vehicle's trajectory, and would want to be able to query the trajectories of those cars to see if they were forced to take any kind of evasive action.  We need to synthesize metrics of "roadway state" such as crowded or light traffic, perhaps identify bunches of cars (even on a lightly driven road we might see a grouping of cars that effectively blocks all the lanes), etc.  Road surface and visibility clearly are relevant, and roadway debris.  We would need some form of composite model covering all of these considerations.

I could elaborate but I'm hoping you can already see that we are looking at a very complicated real-time database question.  What makes it interesting to me is that on the one hand, it clearly does have a great deal of relatively standard structure (like any database): a schema listing information we can collect for each vehicle (of course some "fields" may be populated for only some cars...), one for each segment of the highway, perhaps one for each driver.  When we collect a set of documentation on bad drivers of the month, we end up with a database with bad-driver records in it: one linked to vehicle and driver (after all, a few people might share one vehicle and perhaps only some of the drivers are reckless), and then a series of videos or trajectory records demonstrating some of the "all time worst" behavior by that particular driver over the past month.

But on the other hand, notice that our queries also have an interesting form of locality: they are most naturally expressed as predicates over a series of temporal events that make up a particular trajectory, or a particular set of trajectories: on this date at this time, vehicle such-and-such swerved to pass an 18-wheeler truck on the right, then dove three lanes across to the left (narrowly missing the bumper of a car as it did so), accelerated abruptly, braked just as suddenly and dove to the right...  Here, I'm describing some really bad behavior, but the behavior is best seen as a time-linked (and driver/vehicle-linked) series of events that are easily judged as "bad" when viewed as a group, and yet that actually would be fairly difficult to extract from a completely traditional database in which our data is separated into tables by category.  

Standard databases (and even temporal one) don't offer particularly good ways to abstract these kinds of time-related event sequences if the events themselves are from a very diverse set.  The tools are quite a bit better for very regular structures, and for time series data with identical events -- and that problem arises here, too.  For example, when computing a vehicle trajectory from identical GPS records, we are looking at a rather clean temporal database question, and some very good work has been done on this sort of thing (check out Timescale DB, created by students of my friend and colleague, Mike Freedman!).  But the full-blown problem clearly is the very diverse version, and it is much harder.  I'm sure you are thinking about one level of indirection and so forth, and yes, this is how I might approach such a question -- but it would be hard even so.

In fact, is it a good idea to model a temporal trajectory a database relation?  I suspect that it could be, and that representing the trajectory that way would be useful, but this particular kind of relation just lists events and their sequencing.  Think also about this issue of event type mentioned above: here we have events linked by the fact that they involve some single driver (directly or perhaps indirectly -- maybe quite indirectly).  Each individual event might well be of a different type: the data documenting "caused some other vehicle to take evasive action" might depend on the vehicle, and the action, and would be totally different from the data documenting "swerved across three lanes" or "passed a truck on its blind side."  

Even explaining the relationships and causality can be tricky: Well, car A swerved in front of car B, which braked, causing C to brake, causing D to swerve and impact E.  A is at fault, but D might be blamed by E!

In fact, as we move through the world -- you or me, as drivers of our respective vehicles, or for that matter even as pedestrians trying to cross the road, this aspect of building self-centered domain-specific temporal databases seems to be something we do very commonly, and yet don't model particularly well in today's computing infrastructures.  Moreover, you and I are quite comfortable with highways that might have cars and trucks, motorcycles, double-length trucks, police enforcement vehicles, ambulances, construction vehicles... extremely distinct "entities" that are all capable of turning up on a highway, our standard ways of building databases seem a bit overly structured for dealing with this kind of information.

Think next about IoT scaling.  If we had just one camera, aimed at one spot on our highway, we still could do some useful tasks with it: we could for example equip it with a radar-speed detector that would trigger photos and use that to automatically issue speeding tickets, as they do throughout Europe.  But the task I described above fuses information from what may be tens of thousands of devices deployed over a highway more than 100 miles long at the location I specified, and that highway could have a quarter-million vehicles on it at peak commute hours.

As a product opportunity, Smart Highways Inc is looking at a heck of a good market -- but only if they can pull off this incredible scaling challenge.  They won't simply be applying their AI/ML "driving quality" evaluation to individual drivers, using data from within the car (that easier task is the one Hari Balakrisnan's Cambridge Mobile Telematics has tackled, and even this problem has his company valued in the billions as of round A).  Smart Highways Inc is looking at the cross-product version of that problem: combining data across a huge number of sensor inputs, fusing the knowledge gained, and eventually making statements that involve observations taken at multiple locations by distinct devices.  Moreover, we would be doing this at highway scale, concurrently, for all of the highway all of the time.

In my lecture today, we'll be talking about MapReduce, or more properly, the Spark/Databricks version of Hadoop, which combines an open source version of MapReduce with extensions to maximize the quality of in-memory caching and introduces a big-data analytic ecosystem.  The aspect of interest to me is the caching mechanism:  Spark centers on a kind of cacheable query object they call a Resilient Distributed Data object, or RDD.  An RDD describes a scalable computation designed to be applicable across a sharded dataset, which enables a form of SIMD computing at the granularity of files or tensors being processed on huge numbers of compute nodes in a datacenter.

The puzzle for my students, which we'll explore this afternoon, is whether the RDD model could be transferred from the batched, non-real-time settings in which it normally runs (and even more than that, functional, in the sense that Spark treats every computation as a series of read-only data transformation steps, from a static batched input set through a series of MapReduce stages to a sharded, distributed result).  So our challenge is: could a graph of RDDs and an interative compute model express tasks like the Smart Highway ones?  

RDDs are really a linkage between database models and a purely functional Lisp-style Map and Reduce functional computing model.  I've always liked them, although my friends who do database research tend to view them dimnly, at best.  They often feel that all of Spark is doing something a pure database could have done far better (and perhaps more easily).  Still, people vote with their feet and for whatever reason, this RDD + computing style of coding is popular.

So... could we move RDDs to the edge?  Spark itself, clearly, wouldn't be the proper runtime: it works in a batched way, and our setting is event-driven, with intense real-time needs.  It might also entail taking actions in real-time (even pointing a camera or telling it to take a photo, or to upload one, is an action).  So Spark per-se isn't quite right here.  Yet Spark's RDD model feels appropriate.  Tensor Flow uses a similar model, by the way, so I'm being unfair when I treat this as somehow Spark-specific.  I just have more direct experience with Spark, and additionally, see Spark RDDs as a pretty clear match to the basic question of how one might start to express database queries over huge IoT sensor systems with streaming data flows.  Tensor Flow has many uses, but I've seen far more work on using it within a single machine, to integrate a local computation with some form of GPU or TPU accelerator attached to that same host.  And again, I realize that this may be unfair to Tensor Flow.  (And beyond that I don't know anything at all about Julia, yet I hear that system name quite often lately...)

Anyhow, back to RDDs.  If I'm correct, maybe someone could design an IoT Edge version of Spark, one that would actually be suitable for connecting to hundreds of thousands of sensors, and that could really perform tasks like the one outlined earlier in real-time.  Could this solve our problem?  It does need to happen in real-time: a smart highway generates far too much data per second to keep much of it, so a quick decision is needed that we should document the lousy driving of vehicle A when driver so-and-so is behind the wheel, because this person has caused a whole series of near accidents and actual ones -- sometimes, quite indirectly, yet always through his or her recklessness.  We might need to make that determination within seconds -- otherwise the documentation (the raw video and images and radar speed data) may have been discarded.

If I was new to the field, this is the problem I personally might tackle.  I've always loved problems in systems, and in my early career, systems meant databases and operating systems.  Here we have a problem of that flavor.

Today, however, scale and data rates and sheer size of data objects are transforming the game.  The kind of system needed would span entire datacenters, and we will need to use accelerators on the data path to have any chance at all of keeping up.  So we have a mix of old and new... just the kind of problem I would love to study, if I was hungry for a hugely ambitious undertaking.  And who know... if the right student knocks on my door, I might even tackle it.

Wednesday, 3 April 2019

The intractable complexity of machine-learned control systems for safety-critical settings.

As I read the reporting on the dual Boeing 737 Max air disasters, what I find worrying is that the plane seems to have depended on a very complicated set of mechanisms that interacted with each other, with the pilot, with the airplane flaps and wings, and with the environment in what might think of as a kind of exponentially large cross-product of potential situations and causal-sequence chains.  I hope that eventually we'll understand the technical failure that brought these planes down, but for me, the deeper story is already evident, and it concerns the limits on our ability to fully specify extremely complex cyber-physical systems, to fully characterize the environments in which they need to operate, to anticipate every plausible failure mode and the resultant behavior, and to certify that the resulting system won't trigger a calamity.   Complexity is the real enemy of assurance, and the failure to learn that lesson can result in huge loss of lives.

One would think that each event of this kind would be sobering and lead to a broad pushback against "over-automation" of safety-critical systems.  But there is a popular term that seemingly shuts down rational thinking: machine learning.

The emerging wave of self-driving cars will be immensely complex -- in many ways, even more than the Boeing aircraft, and also far more dependent upon a high quality of external information coming from systems external to the cars (from the cloud).  But whereas the public seems to perceive the Boeing flight control system as a "machine" that malfunctioned, and has been quick to affix blame, it doesn't seem as if accidents involving self-driving cars elicit a similar reaction: there have been several very worrying accidents by now, and several deaths, yet the press, the investment community and even the public appear to be enthralled.

This is amplified by ambiguity about how to regulate the area.  Although any car on the road is subject to safety reviews both by a federal organization called the NHTSA and by state regulators, the whole area of self-driving vehicles is very new.  As a result, these cars don't undergo anything like the government "red team" certification analysis required for planes before they are licensed to fly.  My sense is that because these cars are perceived as intelligent, they are somehow being treated differently from what we perceive as a more mechanical style of system when we think about critical systems on aircraft, quite possibly because machine intelligence brings such an extreme form of complexity that there actually isn't any meaningful way to fully model or verify their potential behavior.  Movie treatments of AI focus on themes like "transcendence" or "exponential self-evolution" and in doing so, they both highlight the fundamental issue here (namely, that we have created a technology we can't truly characterize or comprehend), while at the same time elevating it to human-like or even superhuman status.

Take a neural network: with even a few nodes, today's neural network models become mathematically intractable in the sense that although we do have mathematical theories that can describe their behavior, the actual instances would be too complex to model.  Thus one can definitely build such a network and experiment upon it, but it becomes impossible to make rigorous mathematical statements.  In effect, these systems are simply too complex to predict their behavior, other than by just running them and watching how they perform.  On the one hand, I suppose you can say this about human pilots and drivers too.  But on the other hand, this reinforces the point I just made above: the analogy is false, because a neural network is very different than an intelligent human mind, and when we draw that comparison we conflate two completely distinct control models.

With safety critical systems, the idea of adversarial certification, in which the developer proves the system safe while the certification authority poses harder and harder challenges, is well established.  Depending on the nature of the question, the developer may be expected to use mathematics, testing, simulation, forms of root-cause analysis, or other methods.  But once we begin to talk about systems that have unquantifiable behavior, and yet that may confront stimuli that could never have been dreamed up during testing,  we enter a domain that can't really be certified for safe operation in the way that an aircraft control system normally would be -- or at least, would have been in the past, since the Boeing disasters suggest that even aircraft control systems may have finally become overwhelmingly complex.

When we build systems that have neural networks at their core, for tasks like robotic vision or robotic driving, we enter an inherently uncertifiable world in which it just ceases to be possible to undertake a rigorous, adversarial, analysis of risks.

To make matters even worse, today's self-driving cars are designed in a highly secretive manner, tested by the vendors themselves, and are really being tested and trained in a single process that occurs out on the road, surrounded by normal human drivers, people walking their dogs or bicycling to work, children playing in parks and walking to school.  All this plays out even as the systems undergo the usual rhythm of bug identification and correction, frequent software patches and upgrades: a process in which the safety critical elements are continuously evolved even as the system is developed and tested.

The government regulators aren't being asked to certify instances of well-understood control technologies, as with planes, but are rather being asked to certify black boxes that in fact are nearly as opaque to their creators as to the government watchdog.  No matter what the question, the developer's response is invariably the same: "in our testing, we have never seen that problem."  Boeing reminds us to add the qualifier: "Yet."

The area is new for the NHTSA and the various state-level regulators, and I'm sure that they rationalize this inherent opacity by saying to themselves that over time, we will gradually develop  safety-certification  rules -- the idea that by its nature, these technologies may not permit a systematic certification seems not to have occurred to the government, or the public.  And yet a self-driving car is a 2-ton robot that can accelerate from 0 to 80 in 10 seconds.

You may be thinking that well, in both cases, the ultimate responsibility is with the human operator.  But in fact there are many reasons to doubt that a human can plausibly intervene in the event of a sudden problem: people simply aren't good at reacting in a fraction of a second.  In the case of the Boeing 737 Max, the pilots of the two doomed planes certainly weren't able to regain control, despite the fact that one of them apparently did disable the problematic system seconds into the flight.  Part of the problem relates to unintended consequences: apparently, Boeing recommends disabling the system by turning off an entire set of subsystems, and some of those are needed during takeoff, so the pilot was forced to reengage them, and with them, the anti-stall system reactivated. A second issue is just the lack of adequate time to achieve "affirmative control:"  People need time to formulate a plan when confronted with a complex crisis outside of their experience, and if that crisis is playing out very rapidly, may be so overwhelmed that even if a viable recovery plan is available they might fail to discover it.

I know the feeling.  Here in the frosty US north, it can sometimes happen that you find that your car is starting to skid on icy, snowy roads.  Over the years I've learned to deal with skids, but it takes practice.  The first times, all your instincts are wrong: in fact for an unexperienced driver faced with a skid, the safest reaction is to freeze.  The actual required sequence is to start by figuring out which direction the car is sliding in (and you have to do this while your car is rotating).  Then you should  steer towards that direction, no matter what it happens to be.  Your car should straighten out, at which point you can gently pump the brakes.  But all this takes time, and if you are skidding quickly, you'll be in a snowbank or a ditch before you manage to regain control.  In fact the best bet of all is to not skid in the first place, and after decades of experience, I never do.  But it takes training to reach this point.  How do we train the self-driving machine learning systems on these rare situations?  And keep in mind, every skid has its very own trigger.  The nature of the surface, the surroundings of the road, the weather, the slope or curve, other traffic -- all factor in.

Can machine learning systems powered by neural networks and other clever AI tools somehow magically solve such problems?

When I make this case to my colleagues who work in the area, they invariably respond that the statistics are great... and yes, as of today, anyone would have to acknowledge this point.  Google's Waymo has already driven a million miles without any accidents, and perhaps far more because that number has been out there for a while.

But then (sort of like with studies of new, expensive, medications) you run into the qualifiers.  It turns out that Google tests Waymo in places like Arizona, where roads are wide, temperatures can be high, and the number of people and pets and bicyclists would often be rather low (120F heat doesn't really make bicycling to work all that appealing).   They also carefully clean and tune their cars between each test drive, so the vehicles are in flawless shape.  The also benefit simply because so many human drivers shouldn't be behind the wheel in the first place: Waymo is never intoxicated, isn't likely to be distracted by music, phone calls, texting, arguments between the kids in the back.  It has some clear advantages even before it steers itself from the parking lot.

Yet there are easy retorts:
  • Let's face it: conditions in places like Phoenix or rural Florida are about as benign as can be imagined.  In any actual nationwide deployment, cars would need to cope with mud and road salt, misaligned components, power supply issues (did you know that chipmunks absolutely love to gnaw on battery wires?).  Moreover, these vehicles had professional drivers in the emergency backup role, and focused attentively on the road and the dashboard while being monitored by a second level of professionals with the specific role of reminding them to pay attention.  In a real deployment, the human operator might be reading the evening sports results while knocking back a beer or two and listening to the radio or texting a friend.  
  • Then we run into issues of roadwork that invalidates maps and lane markings, GPS signals are well known to bounce off buildings, resulting in echoes that can confuse a location sensor (if you have ever used Google Maps in a big city, you know what I mean).  Weather conditions can result in vehicle challenges never seen in Phoenix: blizzard conditions, flooded or icy road surfaces, counties that ran low on salt and money for plowing and left their little section of I87 unplowed in the blizzard, potholes hiding under puddles or in deep shadow, tires with uneven tread wear or that have gone out of balance, and the list is really endless.  On the major highways near New York, I've seen cars abandoned right in the middle lane, trashcans upended to warn drivers of missing manhole covers, and had all sorts of objects fly off flatbed trucks right in front of me: huge metal boxes, chunks of loose concrete or metal, a mattress, a refrigerator door...  This is the "real world" of driving, and self-driving cars will experience all of these things and more from the moment we turn them loose in the wild.
  • Regional driving styles vary widely too, and sometimes in ways that don't easily translate from place to place and that might never arise in Phoenix.  For example, teenagers who act out in New Jersey and New York are fond of weaving through traffic.  At very high speeds.  In Paris, this has become an entire new concept in which motorcyclists get to use the lanes "between" the lanes of cars as narrow, high-speed driving lanes (and they weave too).  But New Jersey has its version of a weird rule of the road too: on the main roads near Princeton, for some reason there is a kind of sport of not letting cars enter from, and even elderly drivers won't leave you more than a fraction of a second and a few inches to spare as you dive into the endless stream.  I'm a New Yorker, and can drive like a taxi driver there... well, any New York taxi driver worth his or her salary can confirm that this is a unique experience, a bit like a kind of high-speed automotive ballet (or if you prefer, like being a single fish in a school of fish).  The taxis flow down the NYC avenues at 50mph, trying to stay with the green lights, and flowing around obstacles in a strangely coordinated ways.  But New York isn't special. Over in Tel Aviv, drivers will switch lanes without a further through after glancing no more than 45 degrees to either side, and will casually pull in front of you leaving centimeters to spare.  Back in France, at the Arc de Triomphe and Place Victor Hugo, the roundabouts allow incoming traffic in priority over outgoing traffic... but only those two use this rule; in all the rest of Europe, the priority favors outgoing traffic (this makes a great example for teaching about deadlocks!)  And in Belgium, there are a remarkable number of unmarked intersections.  On those, the priority always allows the person entering from the right to cut in front of the person on his/her left even if the person from the right is crossing the street or turning, and even if the person on the left was on what seemed like the main road.  In Province, the roads are too narrow: everyone blasts down them at 70mph but also is quick to actually go off the road, with one tire on the grass, if someone approaches in the other direction.  If you didn't follow that rule... bang!  In New Dehli and Chennai, anything at all is accepted -- anything.  In rural Mexico, at least the last time I was there, the local drivers enjoyed terrifying the non-local ones (and I can just imagine how they would have treated robotic vehicles).   
And those are just environmental worries.  For me, the stranger part of the story is the complacency of the very same technology writers who are rushing to assign blame in the recent plane crashes.  This gets back to my use of the term "enthralled."  Somehow, for them, the mere fact that self-driving cars are "artificially intelligent" seems to blind technology reviewers to the evident reality: namely, that there are tasks that are far too difficult for today's machine learning solutions, and that they simply aren't up to the task of driving cars -- not even close!

What, precisely, is the state of the art?  Well, we happen to be wrapping up an exciting season of  faculty hiring focused on exactly these areas of machine learning.  In the past few weeks I've seen talks on vision systems that try to make sense of clutter or to anticipate what might be going on around a corner or behind some visual obstacle.  No surprise: the state of the art is rather primitive.  We've also heard about research on robotic motion just to solve basic tasks like finding a path from point A to point B in a complex environment, or ways to maneuver that won't startle humans in the vicinity.

Let me pause to just point out that if these basic tasks are considered to be cutting edge research, shouldn't it be obvious that the task of finding a safe path, in real-time (cars don't stop on a dime, you know), is actually not a solved one, either.  If we can't do it in a warehouse, how in the world have we talked ourselves into doing it on Phoenix city streets?

Self-driving cars center on deep neural networks for vision, and yet nobody quite understands how to relate the problem these devices solve to the real safety issue that cars confront.  Quite the opposite: neural networks for vision are known to act bizarrely for seemingly trivial reasons.  A neural network that is the world's best for interpreting photos can be completely thrown off by simply placing a toy elephant somewhere in the room.  A different neural network, that one a champ at making sense of roadway scenes, stops recognizing anything if you inject just a bit of random noise.  Just last night I read a report that Tesla cars can be tricked to veer into oncoming traffic if you put a few spots of white paint on the lane they are driving down, or if the lane marking to one side is fuzzy.  Tesla, of course, denies that this could ever occur in a real-world setting, and points out that they have never observed such an issue, not even once.

People will often tell you that even if the self-driving car concept never matures, at least it will spin some amazing technologies out.  I'll grant them this: the point is valid.

For example, Intel's Mobile Eye is a genuinely amazing little device that warns you if the cars up ahead of you suddenly brake.  I had it in a rental car recently and it definitely avoided a possible read-ender for me new Newark airport.  I was driving on the highway when a the wind blew a lot of garbage from a passing truck.  Everyone (me included) glanced in that direction, but someone up ahead must have also  slammed on the brakes.  A pileup was a real risk, but Mobile Eye made this weird squack (as if I was having a sudden close encounter with an angry duck), and vibrated the steering wheel, and it worked: I slowed down in time.

On the other hand, Mobile Eye also gets confused.  A few times it through I was drifting from my lane when actually, the lane markers themselves were just messy (some sort of old roadwork had left traces of temporary lane markings).  And at one point I noticed that it was watching speed limit signs, but was confused by the speed limits for exit-only lanes to my right, thinking that they also applied to the thru traffic lanes I was in.

Now think about this: if Mobile Eye gets confused, why should you assume that Waymo and Tesla and Uber self-driving cars never get confused?  All four use neural network vision systems.  This is a very fair question.

Another of my favorite spinouts is Hari Balakrishnan's startup in Boston.  His company is planning to monitor the quality of drivers: the person driving your car and perhaps those around your car too.  What a great idea!

My only worry is that if this were really to work well, could our society deal with the consequences?  Suppose that your head-up display somehow drew a red box around every dangerous car anywhere near you on the road.  On the positive side, now you would know which are were being driven by hormonal teenagers, which have drivers who are distracted by texting, which are piloted by drunk or stoned drivers, which have drivers with severe cataracts who can't actually see much of anything...

But on the negative side, I honestly don't know how we will react.  The fact is that we're surrounded by non-roadworthy cars, trucks carrying poorly secured loads of garbage,  and drivers who probably should be arrested!

Then it runs the other way, too.  If you are driving on a very poor road surface, you might be swerving to avoid the potholes or debris.  A hands-free phone conversation is perfectly legal, as is the use of Google Maps to find the address of that new dentist's office.  We wouldn't want to be "red boxed" and perhaps stopped by a state trooper for reasons like that.

So I do hope that Hari can put a dent in in road safety.  But I suspect that he and his company will need quite a bit of that $500M they just raised to pull it of.

So where am I going with all of this?  It comes down to an ethical question.  Right this second, the world is in strong agreement that Boeing's 737 Max is unsafe under some not-yet-fully-described condition.  Hundreds of innocent people have died because of that.  And don't assume that Airbus is somehow different -- John Rushby could tell you some pretty hair-raising stories about Airbus technology issues (their planes have been "fly by wire" for decades now, so they are not new to the kind of puzzle we've been discussing).  Perhaps you are thinking that well, at least Airbus hasn't killed anyone.  But is that really a coherent way to think about safety?

Self-driving cars may soon be carrying far more passengers under far more complex conditions than either of these brands of air craft.  And in fact, driving is a much harder job than flying a plane.  Our colleagues are creating these self-driving cars, and in my view, their solutions just aren't safe to launch onto our roads yet.  This generation of machine learning may simply not be up to the task.  Our entire approach to safety certification isn't yet ready to cope with the needed certification tasks.

When we agree to allow these things out on the road, that will include roads that you and your family will be driving on, too.  Should Hari's company put a red warning box around them, to help you stay far from them?  And they may be driving on your local city street too.  Your dog will be chasing sticks next to that street, your cats will out there doing whatever cats do, and your children will be learning to bicycle, all on those same shared roads.

There have already been too many  deaths.  Shouldn't our community be calling for this to stop, before far more people get hurt?

Sunday, 20 January 2019

Derecho status update

As we swing into 2019 mode, I wanted to share a quick Derecho status report and point to some goals for the coming months.

First, our ACM Transactions on Computer Sysms paper will be appearing sometime soon, which should give nice visibility for the work, and also the validation that comes from a tough peer-to-peer reviewing process.  The paper has hugely improved through the pushback our reviews provided, so it was a challenge but, I think, worth it.  The system itself works really well!

Next, we are starting to focus on a stronger integration with Azure IoT, where Derecho could be used either as a tool for creating new micro-services with strong fault tolerance and consistency guarantees, or as an ultra fast RDMA-capable object store.  Microsoft has been supportive of this and Derecho should be available from their third party portal, still as a free and open source technology.

But that portal isn’t available yet.  So right now, use Derecho via the  v0.9 release of the system, which will be available by February 1 (we are saving v1.0 for later in the year, after we have a reasonable amount of end user experience).  As of today, we still have one or two bugs we want to fix before doing that release.

Some key points:

  • We are urging people to use the Ubuntu Linux version, because this interoperates between normal Linux environments and Azure (the Microsoft cloud).  On our release site (download here), you can find the source code but also some VMs (a container and then a true VM) with the library preinstalled.  But in fact Derecho should work on any Linux-compatible system.
  • Right now, Derecho has only been tested in a single cluster, cloud (Azure, including Azure IoT, AWS, etc).  We have some limited experience with virtualization, and with ROCE as opposed to pure Infiniband.
  • The easiest path to using Derecho is via the new key-value store.  In this both keys and values can be any serializable object type you like, and we offer a wide range of features: Put and Get, but also a conditional put, which checks that the version you are writing was based on the most current version of the underlying object (useful for atomic replace, like in Zookeeper), plus a watch operation that works just like a topic based pub-sub or DDS.  Objects can be stateless, stateful but not versioned, or versioned and persistent with strong consistency and extremely accurate temporal indexing.  On this we will eventually support pub-sub (think of Kafka or OpenSplice), file systems (HDFS, Ceph), and maybe even a genuine Zookeeper look-alike.  The only caution is that the watch feature isn’t designed to support huge numbers of watched topics.  So if you would have more than 50 or 100 active topics, consider using Dr. Multicast to squeeze that set down.
  • The full system can only be used directly from our templates library API in C++, but you can easily build a wired-down library with no templated methods and then load it from Java or Python or whatever.
  • Runs on RDMA, OMNIPath, and even on normal TCP with no special hardware help at all.  You just configure it via a configuration file, to tell the system how to set itself up.  We use LibFabrics for this mapping to the underlying hardware.
  • Right now, all the Derecho group members need to be on hardware with identical endian and byte alignment policies, but clients not in the group can use RESTful RPC, the OMG DDS stack, WCF or JNI to issue RPCs to Derecho group members, which can then relay the request as appropriate.  
Later this year we will extend the system in various ways.  The API should stay stable, but the new  features would include:
  • Hierarchically structured WAN layer that does read-only content mirroring for the object store.
  • A form of ultra fast and scalable LAN and WAN BlockChain support.
  • Machine checked correctness proofs, and a reference-version of the core Derecho protocols both in a high level form, and as proved and then re-extracted from those proofs in C or C++.
  • External client access to our API via RDMA, supporting point-to-point send and query.
  • Integration with Matt Milano’s mobile code language, MixT, allowing a client to send code to data residing in the object store.

Tuesday, 29 August 2017

The adequacy of specifications

I had coffee with a visitor yesterday: Professor Eva Kuhn from the Technical University in Vienna.  Our conversation was focused on the power, and limitations, of new methods for creating correct solutions to distributed computing problems.

As you probably know, for many years I've been in dialog with a number of programming language researchers (notably Bob Constable, Mooly Sagiv and Noam Rimsky, although the full list would be  much longer and would include Leslie Lamport, Nancy Lynch, Jay Lorch and many others), all specialists on a new way of generating provably correct distributed computing systems and protocols from formal specifications.  I'm not an expert on this topic myself -- my close collaborator Robbert van Renesse is far more knowledgeable than me, and actually works with such tools himself.  Call me an enthusiast.

The methodology they've worked with is roughly as follows.  Using temporal logic or a similar abstract mathematical representation, one creates a description of the problem in terms of sets (the members might be understood as computing nodes, processes, variables, the network itself -- the designer gets to decide), operations upon them, and statements about them.  In this way we can model a distributed collection of computers, exchanges of messages between processes running upon them, and even crashes. 

Next, one specifies a desired behavior, such as uniform agreement (the abstract problem underlying consensus protocols such as Paxos, including the versions we built into Derecho).  In some sense this step describes a "goal", but not the method for achieving the goal.  Think of the specification as a set of constraints, assumptions, invariants: properties that characterize a correct solution.  Ideally, the behavior would have a safety component ("the solution only does good things, in the following sense...") and a liveness component ("provided that the following assumptions hold, the solution always terminates").  But some protocols aren't always live, and sometimes the conditions under which they are live are difficult to pin down, so this second aspect isn't necessarily feasible.
At any rate, in the penultimate step, one specifies the desired protocol itself, but still in a logic formalism.  This is done by expressing the behavior of the protocol as a sequence of operations in the underlying framework -- for example, as a set of temporal logic "actions" on the underlying sets, carefully limited so that any "distributed" operation is performed using our abstracted versions of primitives that make sense in real networks.  For example, the standard Paxos protocol, with its leader-based rounds used to construct ballots and contend for slots in the Paxos log, would be transformed into a series of set operations that match the behavior of the leader, the local copies of the logs at each of the acceptor processes, and so forth.  The lowest level operations would be formal versions of message send and receive primitives.

With this in hand, the next step is to use a theorem prover like NuPRL (Constable's system) or Ivy (the one used at Tel Aviv University) to prove that the abstractly-specified protocol implements the abstractly-formalized behavioral specification.  For example, in the case of Paxos, such a proof would show that for any feasible mix of roles (leader, acceptor, etc), and for every reachable protocol state, the correctness invariants hold.  We would also want to show that from any initial state, some decision states are always reachable, but of course this is not always possible.  For one thing, the FLP impossibility prevents us from creating a protocol in which a decision is guaranteed to occur within finite time, but in fact there are similar cases in which progress can't occur, namely situations that might involve a crash of a majority of the machines, or a partitioning of the network.   For example, if you were to launch a consensus algorithm in a setting where more than half the nodes have crashed, clearly it wouldn't be able to reach consensus.  As mentioned above, in the ideal case you actually specify assumptions under which progress can occur ("we assume that at least a majority of the processes are operational and remain operational throughout the execution of the protocol"), but it isn't always as easy as you might expect to specify those assumptions.  So sometimes, this aspect is not addressed.

These NuPRL or Ivy (or TLA+, Dafny, Coq, Larch...) proofs are semi-manual. There is a proof-checking step, typically done using a technique called model checking (basically, the system enumerates reachable states and verifies that the invariants hold for all such states).  Then there are higher level theorems that can offer short-cuts: general proof cases that were previously proved and checked that essentially represent forms of meta-reasoning, covering a class of behaviors.  These allow the checker to avoid repeatedly model-checking basic steps and to instead model-check the pattern, and then look for instances of that pattern.  Finally, when the checker stalls, a human can intervene and help it find the proof (or perhaps modify the protocol or the target environment specification, to make it easier to establish the desired property). 

The meta-proofs (the higher level ones) are very interesting and necessary, because they potentially address cases that cannot be model-checked by exhaustively enumerating every reachable state.  For example, suppose that some protocol can generate unbounded runs of states, but a proof exists that every reachable state satisfies a given property.  With that "meta" proof in hand, we don't need to examine every reachable state in order to know that the property always holds, and this might let us make a true statement about the protocol that references the meta-property. In contrast, had we tried to examine every reachable state, the checker would have failed, since the runs are unbounded, hence the number of states needing to be checked is unbounded. 
In practice, the power of a tool like Ivy or NuPRL centers on this kind of meta-reasoning, and the sophistication of the tactics used to match proof requirements to the library of meta-proofs.  Someday, these tactics may approach the sophistication of a human logician, and in fact NuPRL has already been used to semi-automatically solve some deep open problems in logic!  But there are many cases it would not yet be able to tackle.

When checkers fail, they sometimes can exhibit a counterexample: perhaps, a run in which two processes enter "decision" states but hold different outcome values, violating consensus.  But they can also simply fail to find a proof.  This is because a powerful enough specification language can encode undecidable questions, hence one simply cannot automate the entire proof task: there are guaranteed to be some problems on which a prover can neither conclude that a statement is true, nor false.  Moreover, for any finite amount of resources (space, computer time) there are problems that would take much more space, or much more time, to model check.  So for several reasons, the checker might stall.  If it succeeds, though, the result is that we have a proof for our abstract protocol specification: we can show that it solves the problem, as specified.

An interesting point, tangential to what I really want to say here, is that one could perhaps extract minimum conditions for progress (a form of weakest precondition), in the manner common in PL correctness proofs of a few decades ago.  This would automate extraction of assumptions needed to prove "conditional liveness": if the precondition holds, then progress will occur. To me that would be amazing, and would automate a step that Chandra and Toueg first proposed for consensus nearly 20 years ago (the famous <>W oracle).  If you love theory and languages, do consider tackling this challenge!

But staying "on message", the last step with a prover such as Ivy or NuPRL is to extract a provably correct program in C or O'CaML from the proof itself.  That is, given a specification of the problem, and a specification of the protocol, and a proof that the given protocol solves the problem, these tools let you push a button and automatically extract the corresponding code in an executable form, after which you simply compile and run it!  Ideally, the compiler used should be proved correct (there is a proved compiler for a subset of C), and the operating system itself be proved correct (like SEL4), and the hardware verified too (using tools like Verilog) and the foundry that made the chips... well, one goes as far as one can.  In fact any chain of technologies has its limitations.  But let's not fuss over the obvious.

Professor Kuhn works with people developing safety critical systems for self-driving cars, control of potentially dangerous equipment, and so forth, and for her, this new methodology was fascinating.  In fact she isn't the first person I've talked to about this: Chris Hobbs, at QNX, and his colleague Peter Shook, are also extremely interested in the potential of such tools.  By taking the programmer out of the loop and extracting code directly from a proof. we seemingly eliminate a weakness in many kinds of control systems, where one historically would hire a team to design a solution, but then would depend on people to write the required code, after which you use a method such as the "B method" to try an prove the code correct. The resulting human-generated proofs are only as good as the human team carrying them out, and the worry always exists that they might have failed to check some important case.  With a computer-generated proof, there are computable "checking" methods that can quickly establish whether or not every case was model-checked.
And yet even with automated extraction, issues remain.  Can every solvable problem be tackled in this way?  Over coffee, Professor Kuhn and I talked about two concerns. 
First, there are solvable problems for which a model-checker might run low on space or time and throw up its hands, and hence that could be solved in principle, but in fact might not be amenable to formal treatment even so.  So one can imagine situations in which there is some important task, like controlling the flaps on an airplane wing, a good solution that our engineering colleagues want to implement, and a hand-built proof of correctness that "seems" adequate, but for which there isn't any feasible fully-machine checked counterpart, because our computers might not be powerful enough, or perhaps because our techniques for generating model-checked proofs might not have the needed meta-proof methods at hand.

A related issue was raised by Hobbs and Shook at QNX: If a proof (and for that matter, the corresponding C program) is not "natural" in appearance, a human skeptic might not be easily convinced that it is correct.   Thus there are also model-checked proofs that might be rejected by a team tasked with confirming that the airplane is safe to fly: the computer says "yes, here is the proof" but the skeptic in the team might worry that if no human can read and fully understand that proof, it could be flawed in some systematic way and yet this would be overlooked.
That concern leads directly to the second question Professor Kuhn and I found intriguing.  Our conversation ended on a related form of impasse: suppose that the original problem specification itself is somehow inadequate?  For example, one could imagine a specification for behavior of flaps on an airplane wing that leaves out some important case that can actually arise, and hence fails to pin down the correct behavior in that case.  Such a specification leaves undefined the correct behavior for some actual situations that might arise in the real world, although perhaps it covers "most" cases and hence might seem complete and useful: you could still generate code, look at examples, trace the logic, and see that for those examples the code behaves properly.  The lurking danger would be that because there were unspecified but real cases, examples could also exist in which the behavior would be different than intended, because the specification neglected to cover them.
Thus we would want to be sure that the specification itself was adequate in the sense of fully specifying every case that could really arise in practice.  This, though, seems to be a somewhat less fully solved problem.  Indeed, it seems to pose an impossible requirement!

I've been shown some work that looks at specifications, and the question is a classic one: large communities are hard at work on the topic, and have been for decades.  The issue is that the "adequacy of a specification" problem itself seems to be undecideable.  The intuition is sort of obvious: if one could decide all possible adequacy situations, what would stop me from encoding some simple undecideable problem (such as the halting problem), and then using the test of adequacy to solve the undecideable problem?  Seemingly, nothing stops me from doing this.  Thus adequacy-testing should itself be undecideable.  I bet someone has proved this, although I don't think I've ever seen such a paper.  I need to read more of the PL literature.

At any rate, what we see here is that on the one hand, our field seems to be at the edge of a major advance (automated synthesis of provably correct solutions to safety-critical systems problems), but on the other hand, is also approaching a natural and final form of impossibility: the risk that for important cases, it may turn out to be impossible to verify that the specification itself is "complete".

There is reason for hope.  There are many situations in which if one is given a program and must answer a question about it, the task cannot be solved because the given program might encode an undecideable task.  Yet when we use computational methods to generate programs, we can often prove that our methods only generate sound programs. 
Could we solve the adequacy problem in this manner?  For example, is there a way to generate specifications through some kind of dialog with the developer, that would only generate adequate specifications with full coverage of the problem domain?  This, I think, should be possible.  The resulting solution might not be able to specify every problem you can dream up, but for the things it could specify, we would know that the specification doesn't overlook any possible scenarios.
Perhaps the practical class of critical control systems doesn't actually require the ability to specify control tasks that encode undecideable questions.  If so, then perhaps every needed critical control solution can be created.  This would finesse the issue: even though there may be ways to encode undecideability into the same formalism, our more limited use of the methodology would never attempt to do the impossible.
My hope is that we are rapidly heading towards this kind of happy outcome... with all the progress on proofs using NuPRL an Ivy (and other systems like TLA+, Dafny, Larch and Coq), we'll know pretty soon.

Saturday, 15 July 2017

How far could a secure Internet get us?

There is a standard refrain among those who teach and do research on security: it holds that the fundamental flaw in security originates with an early decision by the community that created the Internet.  In that early design, Internet routing occurs by a form of peering that can often occur anonymously.  Endpoint systems are not authenticated, and packets generally aren't encrypted or authenticated either.  As a consequence, packets are routed permissively even if they contain what are almost certainly false origin addresses, or have content that seems dubious in obvious ways (like a TCP connection packet that makes no sense on this particular link).

This story then holds that the original sin of the Internet design community has given us layer upon layer of infrastructure that cannot be secured because it resides on a flawed and easily compromised foundation.

As it turns out, there is little doubt that we actually can build an Internet that corrects that deep flaw, and that can be relatively compatible with the existing Internet.  Enterprises like military systems and security-conscious companies do it all the time.   Let me sketch out how this is done (it isn't rocket science, and you won't find many surprises).  But then let's ask if it would really be a game-changer for the security of higher level applications.

To appreciate the core challenge, it helps to start by understanding that everything you think you know about the network is really just an abstraction layered over something more basic.  For example, even my advanced students tend to think of Internet addresses as identifiers, as if my computer's true name were 128.84.16.001 and your computer's true name was 167.88.194.023.  In fact, these addresses are better understood as routing data: useful for deciding what the next hop should be as a packet progresses hop-by-hop through the network, but lacking any deep connection to identity. 

In fact, a single computer might have many network addresses (one for each of its network interfaces).  It might host multiple virtual machines, and those could each have virtual network addresses of their own: with virtualization, any computer can function as a kind of Internet and host large numbers of computers that run within it, complete with virtual networks, virtual name spaces, services of various kinds, you name it.  A single computer might move about, so that over short periods of times it takes on a sequence of addresses: the old addresses can cease to work, and traffic needs to be redirected to the new ones.  Addresses can be mapped by network address translators.

Once we free ourselves from this false equivalence of network address to identity, you need to ask what the real root of identity should be, in a modern system.  Here, the proper focus is on hardware security tokens combined with human users who authenticate themselves in the usual ways.  The hardware could be a built-in component of the computer, or it could be some form of plug-in.  But the key point is that when we associate authentication with these unforgeable hardware elements, used in tandem, we arrive at a much stronger notion of endpoint identity.  The deep roots of that form of identity reside in key pairs: the identity defines some form of private key, with which information can be authenticated by public components that only have access to the corresponding public key.

This then is our bootstrap opportunity: we live in a vast world of devices: computers, routers, IoT components like video cameras and smart televisions and smart cars, and each element can be understood as either being anonymous (if it lacks the ability to authenticate itself), or capable of proving that it has "authorized access" to some private key.  With that proof, we can consult a vendor-published registry and from that registry, can learn about this endpoint device.  A device can also be registered in secondary registries: when I bring a new router into my smart home, I could register my router as "Ken's router, at his summer cottage on Cayuga Lake".  And now there would be a trustworthy chain of reasoning that would let you convince yourself that certain messages were indeed sent by, or countersigned by, my router.

Sounds familiar?  It should, if you've ever brought your laptop from home to work.  Some companies won't allow you to connect the laptop at all (fearing viruses that your machine might carry), but those that do usually require precisely this sort of authentication and registration.

Given strong authentication, a second opportunity arises whenever we focus on an island of infrastructure that has a coherent owner.  Here on Cayuga Lake, my network provider is part of a broader system owned and controlled by a company that controls a fairly large regional network.  This ISP is paid for its services, and at least in theory, has complete control of every device that can connect directly to it, every router and switch it operates internally, and every network link used to glue them all together.  One can understand the ISP as a kind of military hierarchy: at the core we find a "master and commander" who has absolute control and is the sole source of permissions.  Below the master and commander are a collection of subordinates, to whom restrictive roles have been granted, and way down at the bottom are the common seaman who might permit packets originating in my router to sail the seas of this regional network -- or could block them.

As it happens, today's ISPs are somewhat relaxed about authentication, so one opportunity to secure the network would start by simply enforcing authentication when devices are connected to an ISP.  Today when I buy a new iPhone, I can simply start to use it in my home.  If I was trying to build a much more secure network, at a minimum my router might pop up a screen requiring me to fill in details: who owns this iPhone (and it might want proof: type in your password, your RSA code number, and hold your thumb on the fingerprint reader...)  Perhaps, that regional ISP would do the same and require a second level of device registration.  Military and other nationally critical infrastructure networks work precisely in this way: if you were to take a laptop into a major power plant and connect it to the Ethernet jack in the waiting room while waiting for your appointment with human resources, either it won't connect, or it will give you some form of very limited guest connectivity. 

Think back to the last time you took your laptop to work.  I bet that something along the lines just described happened then, too.  Any organization that takes security at all seriously is careful to track the devices connected to it, and to limit their networking "power".  A military system won't allow you to connect your own machine, at all.  But if you work at Cornell, like I do, you might be able to get permission -- except that your machine will end up registered for use in a specific context, such as from my office in the Computer Science building.  If I were to carry it across the street and connect it to a wall jack in the ECE department, I would be back to square zero.

With enclaves that use authentication, one can take further steps.  Without too much added cost, packets can be cryptographically signed or fully encrypted at the endpoint, yielding various forms of virtual private networks: subnetworks within which communication is safe, but with strong protection against traffic from the outside leaking in, or against intruders managing to read or tamper with data.  Such systems can also filter or block traffic that might try to escape the secure perimeter.

I worked at Microsoft for a few months in 2016, and they adopted this approach.  I could only connect to their system via a secured VPN, and the security perimeter it enforced when I worked from home was very carefully controlled and monitored.  I could continue projects from work while at home, but I could never have wandered the virtual Microsoft network with impunity from outside the office.  In my office, I had somewhat more relaxed access to internal software tools and projects.

This, then, gives some sense of what a secure Internet would look like.  But how secure can such a system really be?

As we push from the lowest layers of hardware and software up to higher levels of abstraction, the numbers of elements of a modern system increase exponentially.  There are dozens of operating systems and each has hundreds of variants and patch levels.  So the very first layer already has a level of diversity measureable in the thousands.  Then there are hundreds of programming tools and languages and services that can run on them, configurable in hundreds of ways, to say nothing of all the management options.  Layer by layer, we bring in a surreal degree of diversity simply by virtue of the choices made by each system designer and vendor.

In settings like military systems, or power grids, a major effort is invested to keep control over the forms of diversity that are actually present in the deployed system.   Individual users aren't permitted to install their own applications, patches are applied in a coordinated way, and monitoring tools are used to notice unexpected behavior that could point to an intrusion.  In contrast, networks used in other settings need to deal with enormous levels of diversity and individual customization.  Like it or not, the network provider simply won't know what the network is being used to do.

It seems to me that this diversity accounts for the insecurity of modern systems, to a far greater degree than the "original sin" of endpoint anonymity and unauthenticated peering.  While the insecurity of the network certainly makes it easier for attackers to mount denial of service attacks or to route spam emails with falsified origin data, those are just the a small aspect of the larger problem.  And that larger problem centers on the exceptionally large attack surface that modern systems offer: hundreds of millions if not billions of lines of code, riddled with bugs, and configured in every imaginable way (just yesterday I was horrified to discover that my home router has an administrative login and password, both set to the defaults.  Now I'm wondering about my television, and my internet box...). 

Fixing the original sin of the Internet genuinely would help in some ways, especially as we move to deploy an Internet of Things with more and more devices playing a diversity of roles in homes, cars, highways and other settings.  We should take that step.  But it is an illusion to imagine that true software security can be achieved by hardening the network itself, because the extreme diversity of uses would overwhelm any systematic attempt to impose security standards and ensure that they are respected.  Attempting to do so would probably create some very frustrated users, and yet would at best raise the bar slightly for one facet of a complex, multi-faceted problem.

More interesting, I think, is to think about diversity as a constructive tool for protecting large, complex systems.  Fred Schneider and I once coauthored an editorial on this topic, and a short paper, and I continue to believe that this was one of our better efforts.  Synthetic diversity, in particular, is a remarkable tool for combatting the wily attacker, who often has a surprisingly limited arsenal of off the shelf exploits and might be blocked by even small "surprises".

The basic idea is simple: just as a compiler takes source code and then can create a variety of executables (depending on the target instruction set, operating system, optimization level selected, etc), we can also "compile" programs to expose various forms of artificial diversity.  We can force the memory layout to look somewhat random (simply by adding random padding to objects allocated dynamically).  We can vary the stack layout and the order in which inputs are delivered if a program receives data from multiple sources.  We can potentially compile one program several ways, and pick the version that will be running today at random within the resulting set.  We can randomize the numbering used for operating systems calls.

Such steps diversity and obfuscate the attackable surface.  The attacker who was using an exploit that overruns an input buffer in a way that triggers a system call to download and then execute a bot will now run into an unpredictable memory location, a buffer that might not overflow, and in any case the system call to read from the network socket might have been remapped to some normally-unassigned code.  These are steps that really can pay off.

VPN security offers opportunities too.  Obviously, surfing the web requires that there be no barriers.  But for an application like a medical system that manages patient records or interacts with a lab, there is no real reason to also be able to surface the web, and there is no reason that random web programs should be able to communicate to that application, either.  VPNs can offer this sort of protection, and if we could deploy them more easily, they could wrap sensitive code in layers of armor.

So count me on the side of those who believe that Internet security can and should be a priority, particularly in critical infrastructure and Internet of Things scenarios.   It really is about time to make Internet authentication a readily available and widely standard function, and to deploy VPN technologies much more actively.  But doing so won't solve the whole problem.  We should also make more of an effort to synthetically diversify the systems we deploy widely, so that the attacker will encounter a bewildering variety of "versions" of any particular software.   

If you can't build a single impregnable castle, the next best thing is to populate a huge city with every imaginable variation on the castle theme.  Put police checkpoints on the roads leading to the city water pumping and power generating systems.  Post signs in a few languages, including some you made up just for this purpose.   Good luck to that hacker: he might break into one system, but doing so won't get him very far before we root him out...

Monday, 24 April 2017

Will smart memory need an ACID model?

This is really part II of my posting on smart memory from ten days ago.

Let's imagine that we've created the ultimate data warehouse, using Derecho.  This warehouse hosts terabytes of persistent memory, It can absorb updates at a staggering rate: hundreds of gigabits per second, has tens of thousands of processors that crunch the data down and then store it as collections of higher level "knowledge models", and is always hungry for more.  

We used to think of data warehouses as respositories for nuggets of data, so perhaps we could call these "muggets:" models, that can now be queried.  Hopefully this term isn't painfully cute.

Next, we imagine some collection of machine learning applications that consume these muggets and learn from them, or compute some sort of response to them.  For example if the muggets represent knowledge collected on the local highway, the queries might be posed by smart cars trying to optimize their driving plans.  "Is it ok with everyone if I shift to the passing lane for a moment?"  "Does anyone know if there are obstacles on the other side of this big truck?"  "What's the driving history for this motorcycle approaching me: is this guy some sort of a daredevil who might swoop in front of me with inches to spare?"  "Is that refrigerator coming loose, the one strapped to the pickup truck way up ahead?"

If you drive enough, you realize that answers to such questions would be very important to a smart car!  Honestly, I could use help with such things now and then too, and my car is pretty dumb.

We clearly want to answer the queries with strong consistency (for a smart car, a quick but incorrect answer might not be helpful!), but also very rapidly, even if this entails using slightly stale data.  In Dercho, we have a new way to do this that adapts the FFFS snapshot approach described in our SOCC paper to run in what we call version vectors, which is how Derecho stores volatile and persistent data. Details will be forthcoming shortly, I promise.

Here's my question: Derecho's kind of data warehouse currently can't support the full ACID database style of computation, because at present, Derecho only has read-only consistent queries against its temporally precise, causally consistent snapshots.  So we have strong consistency for updates, which are totally ordered atomic actions against sets of version vectors, and strong consistency for read-only queries, but not read/write queries, where an application might read the current state of the data warehouse, compute on it, and then update it.  Is this a bad thing?

I've been turning the question over as I bike around on the bumpy, potholed roads here in Sebastopol, where we are finishing up my sabbatical (visiting my daughter, but I've also dropped in down in the valley and at Berkeley now and then).  Honestly, cyclists could use a little smart warehouse help too, around here!  I'm getting really paranoid about fast downhills with oak trees: the shadows invariably conceal massive threats!  But I digress...

The argument that Derecho's time-lagged model suffices is roughly as follows: ACID databases are  hard to scale, as Jim Gray observed in his lovely paper on "Dangers of Database Scalability".  Basically, the standard model slows down as n^5 (n is the number of nodes running the system).  This observation gave us CAP and BASE and ultimately, today's wonderfully scalable key-value stores and noSQL databases.  But those have very weak consistency guarantees.

Our Derecho warehouse, sketched above (fleshed out in the TOCS paper we are just about to submit) gets a little further. Derecho can work quite well for that smart highway or similar purposes, especially if we keep the latency low enough.  Sure, queries will only be able to access the state as of perhaps 100ms in the past, because the incoming database pipeline is busy computing on the more current state.  But this isn't so terrible.

So the question we are left with is this: for machine learning in IoT settings, or similar online systems, are there compelling use cases that actually need the full ACID model?  Or can Maine learning systems always manage with a big "nearly synchronous" warehouse, running with strong consistency but 100ms or so lagged relative to the current state of the world?  Is there some important class of control systems or applications that can probably be ruled out by that limitation?  I really want a proof, if so: show me that omitting the fully ACID behavior will be a huge mistake, and convince me with mathematics, not handwaving... (facts, not alt-facts).

I'm leaning towards the "Derecho would suffice" answer.  But very curious to hear other thoughts...

Wednesday, 7 December 2016

Smart Cars will need Smart Highways


Vendors are building smart cars much as they build web browsers and cloud applications.  But when a browser crashes, nothing bad happens.  If a car malfunctions, people can be killed.  Product liability could reshape the industry, but I don’t think this needs to be a setback (if anything, it may be empowering, for reasons I’ll explain).

How one builds safety-critical systems

I’ve had several opportunities to design distributed computing systems for settings where mistakes  matter.
These projects have to be taken very seriously.  If an air traffic system (human in the loop like in Europe, or partly automated like we do it here in the US) authorizes a flight plan and the pilot trusts that authorization, lives are on the line.  In fact, such systems have built-in redundancy: airplanes, for example, have a collision avoidance system on board (TCAS).  It operates independently, warning the pilot of any possible violation of plane separation rules and telling the pilot what to do.   The ATC system is also backed up: if the French ATC were to go down, control shifts to neighboring countries: Italy, Switzerland, Germany, England, etc.  There are layers and layers of redundancy.  Of course we don’t want to go there: the last thing anyone would want is an air traffic solution that frequently triggers the last-resort collision avoidance solution.  So we use every imaginable technique to harden these kinds of systems.  But when the technology fails even so, there is a fall-back.

Having humans make the ultimate decisions is especially important in systems that include large software components.  In an ATC system, we use Linux and commercial databases and publish subscribe tools.   It we also know that Linux is buggy, and the database subsystem, and the publish subscribe solution, and even the C++ compiler.  We know this.  So the system is built to be internally redundant and distrustful of itself: it just shuts things down, quite aggressively, if they seem to act strangely.  We assume that things mostly work as intended, but we do not make life or death decisions that depend on trusting that this is so.

Further, even with all this paranoia, a ATC system requires close supervision.  Ultimately, each recommended action is scrutinized by human controllers, and for major actions,  human approval is still required before the recommendation is adopted.  This approach matters more and more over the lifetime of such a project: by now this system has been in use nearly 30 years.  Think of all the patches and upgrades that have occurred.  Even if we had mathematical proofs and astonishing levels of testing before we rolled out ATC version 1.0, could we still feel equally confident in version 17.5.1871?  If you don't apply patches, you run with known bugs.  But it is patches introduce new bugs, too!  The same with major new releases of important components.

These same concerns all apply to self-driving cars.  Worse, cars are are easier for hackers to attack, and far more likely to be targeted.  We took many measures to protect the French ATC.  But protecting one system is easy.  Once there are a million cars on the road, all being serviced by random garages twice a year, will there really be any possible justification to trust that the system is working as originally intended?

“It ain’t what you don’t know that gets you in trouble.  It’s what you think you know that just ain’t so.”  (Mark Twain)

I love this Mark Twain quote.  People are always so sure of themselves, especially when they are totally wrong!
No matter how heroic the measures we take, any technical solution to a problem ultimately depends on hardware, on assumptions, on models, and on problem statements.  The people in charge of defining the computational task can get any or all of those wrong.  When we build a solution, we might be building the wrong thing without realizing it, or overlooking important cases that weren’t properly identified. 
I’ve often been given incorrect hardware specifications (and it isn’t unusual to only notice that the specification was wrong when it causes some really bizarre bug).  I’ve discovered at least ten serious compiler bugs over my career, and innumerable operating systems bugs.  Programming languages are notorious for overlooking cases when specifying the correct semantics for the compiler to employ, so even if the compiler wasn’t buggy, the language design itself may be ambiguous in some respects. 
Or suppose we get it right, deploy our system, and it works like a charm.  Success breeds ambition, so before you know it, the way that the system is deployed and used can evolve.  But this evolution over time could easily invalidate some assumption without anyone really noticing.  Thinking about Mark Twain’s point: sometimes, the things you were sure about when you started the project cease to be true down the road.
I could share some hair-raising stories about how such events caused problems in systems I’ve helped build.  But you know what?  There hasn’t been a single time when at the end of the day, those layers of fail-safe protections didn’t ultimately kick in and prevent the system from actually doing any harm.  So my actual experience has been that if you take proper care, and approach mission-critical computing with adequate humility, you can create safe solutions even using fairly complex technologies.

Self-driving cars are taking a different approach, and it worries me.

This brings us to my key concern: Today, some important safety-critical technology areas have started activities that seem to need the same standards that are used in air traffic control, and yet aren’t using those standards.  Specifically, I’m concerned about self-driving cars.   The core of my worry is this: I don’t actually think that it is possible to build a genuinely safe, fully autonomous driving solution.  Even human drivers misjudge one-another’s intent and accidents ensue (to say nothing of situations where a driver is impaired in some way).  Self-driving cars operate in a world populated by those same erratic human drivers, but complicated by their extensive dependency on incredibly complex sensor technologies.  And yet they lack a good fail-safe option, because they are often operating in domains where slamming on the brakes or swerving suddenly is dangerous too.
We never allow airplanes to get into that sort of situation.  If we did, they would bang into each other in mid-air.  Perhaps you watched Breaking Bad, where a deeply depressed air traffic controller actually steered two planes into a collision.  In practice, that couldn’t happen: alarms would go off in the air traffic control center, and separately in the cockpits, and either some other controller would have stepped in, or TCAS would have steered them away from one-another.   The air traffic control system is designed to keep planes from getting dangerously close to one-another.
In contrast, not long ago a self-driving car operated by software developed at Tesla crashed into a truck, killing the driver.  Tesla accepted some blame: a white truck, on a foggy morning with a bright white background, a street with mostly white surrounding buildings, etc.  The car couldn’t find the contours of the truck, and thought it was driving into an empty intersection.  Tesla also put lots of blame on the driver, suggesting that he had been warned about the limits of its vehicles, and shouldn’t have trusted the self-driving system under those conditions.  Because only the driver was killed, and the driver did make a decision to activate the self-driving mode, Tesla has some chance of prevailing if this question ends up decided in court.  Nobody seems to be suggesting that the company bears any major liability.
This is common in computing: it is rare for anyone to accept responsibility for anything.  But I think it is wrong-headed, and in this story, I see vivid evidence that today’s self-driving cars are operating without those layers of redundancy, and without air traffic control.
It doesn’t take insider knowledge to guess that Tesla’s accident foreshadows further such events in the future, by Tesla and other vendors as well.  We are all Teslas, to paraphrase John F. Kennedy.  Sooner or later, a self-driving car will cause an accident in which the owner of the car is definitely not at fault, and in which completely innocent people are killed or severely injured.  Maybe the problem will be the n’th repeat of Testa’s white truck/white sky scenario, or maybe it will be some other vendor, some other scenario, and will be the very first time that the particular model of car, from the particular vendor, was ever exposed to the situation that caused the crash.  Whatever the cause, lawyers will sue (because this is what lawyers do), and those lawsuits will reveal a huge gap between software liability laws (where the vendor is generally not responsible for harm), and the much tougher liability rules used in life and safety-critical systems, like airplane autopilots and cardiac defibrillators. 
If you build part of an air traffic control system, protection comes from using best standard practice, but also from adopting a layered approach to safety: there needs to be a fail-safe backup option.  Self-driving cars take huge risks, and they lack a safe backup.
So my suggestion is that we need to view self-driving cars in this other way: we should subject self-driving car technologies to the sort of extreme oversight used for air traffic control systems, or airplane guidance systems.  And we should hold the vendor responsible for using best standard practice, looking not just at other self-driving car vendors (that could be a race to the bottom), but at other industries too, and specifically air traffic control.
In suggesting this, I need to acknowledge something: the situation actually isn’t completely clear-cut: Self-driving cars are expected to have better safety records than human drivers.  Computers don’t drive after a few drinks, or text while driving, or doze off.  Very likely, accident rates will drop as self-driving cars enter into wide use.  Some are already arguing that this better average behavior should excuse the occasional horrific accident, even if a software bug causes that accident, and even if the car would make the same mistake, again and again, in the identical (but incredibly rare, unbelievably unlikely) conditions.  But I don’t agree.
Notice the apples-to-oranges comparison occurring here.  On the one hand, we have an averaged out statistical argument that self-driving cars are safer.  And on the other, we have bugs and design flaws, and the absolute certainty that someday, a self-driving car will make an actual mistake that, without question, will be the direct cause of a lethal accident.  Can one legitimately use a statistical observation to counter a rigidly factual one?  Does it matter whether or not we can trace the accident to a specific bug, or to a specific failure in a sensor (that is, are Heisenbug’s somehow excusable, but Bohrbugs intolerable)?   Does it matter whether a human driver would have found the road conditions tough?  Or are the only really problematic bugs ones that cause an accident under perfect driving conditions, when the vendor definitely hasn’t warned that the technology would be unsafe to use?  And while on that topic, shouldn’t the vendor’s software disable itself under conditions where it can’t safely be used?  Why should the human driver have to make a guess about what the vehicle can, and cannot, handle safely?
Where computers are concerned, mistakes are inevitable: not only does complex software have bugs, but self-driving cars will additionally depend on specialized sensing equipment: video cameras, GPS systems, miniature radar devices, wireless connections to the “cloud” to get updates about road conditions….  All of these technologies can fail: the video cameras and radars can become dirty, or malfunction during brutal winter weather, or get knocked out of alignment. 
Indeed, a self-driving car might crash for some reason that isn’t directly tied to a software bug.  Any driver knows that a tire can suddenly explode, or something might crash onto the roadway without warning.  But how can software systems be designed to deal with every imaginable hazard?  Some vendors are proposing to just tell the human driver to take over if such a situation arises, but a sudden handoff could easily catch the driver by surprise.  It follows that accidents will happen.  
When humans make mistakes, there is always an element of uncertainty: the defense team works to convince that judge and jury that negligence wasn’t a factor, and if the jury isn’t certain, the defendant is found innocent.  But when faced with identical conditions, software bugs often can be reproduced, again and again.  This sure sounds like negligence by the vendor of the smart car.
Making matters worse, smart cars aren’t designed and tested the way we design and test airplane autopilots or smart-grid control technologies or cardiac pacemakers.  In fact, smart car vendors use the same techniques used to create the software on our mobile phones and desktop computers.  They don’t have much choice: autopilots and cardiac pacemakers are incredibly simple when compared to a self-driving car’s guidance system: not much really happens at 35,000 feet, and the pilot of the plane can always take over if the autopilot senses possible problems.
In contrast, a self-driving car operates under complex, rapidly changing conditions.  For many possible scenarios, it isn’t even clear what the correct action should be.  With such a complex, vague, problem specification, it is impossible to validate a smart car using the safety standards imposed on an airplane autopilot.  That sort of open-ended safety validation may never be possible. 
Could smart highways be the answer?
But there is an alternative.  We don’t need to tolerate an anything-goes mindset.  Imagine that future cities were linked by networks of smart highways.  Such a highway would have a built in and continuously active traffic control system, fully automated, like an air traffic control system but designed to control cars rather than airplanes.  In this approach, we wouldn’t allow self-driving cars to make their own decisions, so the prospect of cars driving themselves down residential neighborhood streets where children and pets are playing would be eliminated.  Instead, self-driving systems would only be engaged while on a smart highway, and even then, would be under control of that highway at all times.   The human driver would take over when exiting the smart highway, and if anything at all were to go wrong, the car would pull over and stop, or the entire highway would simply come to a halt, quickly and safely. 
And this gets to the crux of the matter.  A smart highway can be designed with a safety-first mentality: if safety can’t be assured, then the cars stop.  In contrast, today’s self-driving cars can never be 100% certain that they are driving safely, or even that they are 100% bug free.  They don’t even try. We’re creating a new world that will operate like a sky full of airplanes on autopilot but without guidance from air traffic controllers, and this is a clear recipe for disaster. 
Moreover, a smart highway control system could be built much as we build air traffic control software: with a primary focus on safety and fail-safe behavior, which would shift the onus from vehicles making totally independent decisions towards a model in which the independence of the on-board control system is constrained by an overarching safety policy: Now we would know not simply that the Tesla control system was engaged, but also that the path planning in which it engaged is bounded by a safety envelop that is the same as (or at least consistent with) the one that the truck was using.   We would have a safety model on which the solution depends; if a smart car crashed into a smart truck on a smart highway, it would be crystal clear where the model broke down: perhaps, by not allowing enough stopping distance between vehicles, or perhaps the truck lost control and just at this instant, the car brakes failed.  But we could break the problem down, assign clear responsibility, and if needed, assign liability.
A smart highway also introduces a form of independent witness.  Think of the VW/Audi emission reporting scandal.  What if a smart car were to err, but then was programmed to lie about the inputs on which it based its decisions, or the conditions that led to the crash?  With a smart highway filming the event and perhaps programmed to automatically persist that data in the event of an accident, we would have concrete evidence from an independent witness that could be used to detect this sort of preprogrammed fibbing.
Tesla’s accident makes it clear that blind trust in machine intelligence is a lethal mistake.  The good news is that this particular mistake is one we can still correct, by building smart highways to control the smart cars and mandating that the cars use those solutions.  As technology advances, we’ll see more and more autonomous computing in settings like hospitals, and there is a real risk that if we blink now, weak standards will spill over into other areas that currently demand stringent quality controls.  We really need to get this one right.