Integer Overflow Bug in Boeing 787 Dreamliner
engadget.com
engadget.com
I can't speak to the quality of the A and B level (most critical) code, but the development process for the C level software I was working on definitely could have used a lot of improvement. Messy code, tests and documentation were an afterthought/checkbox item, etc. The incentives were just wrong.
I think there's a ton of room for process innovation in avionics software development. One thing I wanted to build for a long time was a tool for tracing. In theory, every industry requirement (DO-178B, etc) was supposed to trace to a hight level Software Design Document (SDD) requirement, which was supposed to trace to a Software Requirements Document (SRD) requirement, which would trace to a code function. We maintained all of that BY HAND. It was a huge mess. Perfect example of something that could have been an extremely valuable development tool, but ended up just being a hassle to try and maintain.
Then of course there's language choice. C is king, which isn't necessarily a bad thing, but it's certainly not the safest, even in the restricted forms used in avionics. Sadly, my very first ever project as a programmer was porting an Ada codebase to C for the 787 (off by one errors for days...). It's almost cliche to say nowadays, but I would be really excited to see Rust gain some traction in avionics over the next 20 years or so. Because that's how far behind avionics is. We were using Visual Studio 6 in 2011!
I'm telling you, there's money to be made building tools for this stuff. I think a big part of the reason things aren't being improved is that the people in a position to recognize bad process and tooling maybe aren't the type of people to see an opportunity to make money solving the problem rather than putting up with it. I wouldn't associate most of the engineers I knew at Honeywell as the type to stay up until 2AM every night for 3 months working on a side project to pitch to their boss.
I think it's really exciting what's happening in healthcare right now though. The innovative culture is exploding. Ultimately I care much more about what happens in medicine than avionics, as long as planes aren't falling out of the sky every 248 days...
We're actually integrating more and more of our work in to Visual Studio since its tools are excellent. The problem is that the organization needs to validate any tool before we can use it as a part of Quality Management and that process can take forever.
Bizarrely now I am also helping (in a small way) with an innovative healthcare tech project. Maybe many people go through similar trajectories in programming without realizing it.
That said, our software development process is really just a mild adaption of all our other development processes (like ones we use for hardware and reagent development). As I've described it above, it's a pretty standard engineering approach to design control, and there are all sorts of variations on them.
In fact, the FDA makes note of how broad the field of medical devices are, and does not actually enforce any specific design control process, but rather provides a framework for you to develop a process that meets your developmental and regulatory needs. As part of getting FDA approval, your design control process will be audited, as well as how well you followed it. In addition, medical devices are classified into 3 classes, corresponding to patient risk. Our product is currently classified in the lowest risk level, and so we can avoid a lot of additional requirements. As I recall from skimming through the standard (sorry, we only had a hard copy at work.. costs money apparently), higher risk devices with software components must have certain types of tests performed. In our risk class, we have total freedom to define our testing requirements - that said, the rigour of our testing is still under FDA scrutiny, it just means that there are no specific checkboxes to hit (like integration testing for example).
I guess if you want a place to start off, this might be a good place to look: http://en.wikipedia.org/wiki/Design_controls
NASA and the U.S. Military have good guides and white papers on it, which you should be able to find online with a bit of digging.
[1] http://en.m.wikipedia.org/wiki/V-Model_(software_development...
Edit: Oops, misread the comment.
Is that true for all of Boeing? I recall reading about the Lustre synchronous dataflow language being used by Airbus. It apparently allows all sorts of interesting safety guarantees.
This is a symptom that group culture there is interfering with rational decision making around tool use.
Then of course there's language choice. C is king, which isn't necessarily a bad thing, but it's certainly not the safest, even in the restricted forms used in avionics.
This is another symptom. Perhaps it's excusable if there were preexisting libraries/codebase.
It's almost cliche to say nowadays, but I would be really excited to see Rust gain some traction in avionics over the next 20 years or so. Because that's how far behind avionics is. We were using Visual Studio 6 in 2011!
Another indication that group culture is blocking rational decision making about tool/language choice.
Uh, what would you use? As far as I know, the choices are: Assembler, Ada, and C. We're talking about avionics code, here.
C++ is not going to help you in this case. Java will be too slow/unpredictable. Real-Time Java is kind of sketch in my opinion (I could be wrong there). Most everything else is totally out.
Actually I'd probably choose Ada... but there are reasons the industry switched away from Ada.
In that case, "group" may refer to the avionics software industry as a whole.
At least, that's what I remember hearing---can't really vouch for it and I'd be happy to see someone else weigh in.
Also, my understanding was that Ada was basically forced on the defense industry by the Pentagon, and then there was eventually a backlash, and they dropped it. It may have had more success if it had been adopted voluntarily all along. In fact, it may yet have a resurgence. I know there is at least one serious Ada vendor out there still.
So they went to C? There's some irrational component in there somewhere.
What about Swift? Reference counting has good properties for real time applications. The toolchain is excellent for implementing verification tools. It has fairly high performance, combined with a very large and growing developer base. If someone put together a toolchain for Swift that covered the most useful 20% of features provided by Ada in that context, then such a thing could take over avionics programming.
everything this complicated has always had these problems, difference is news jumps on it like a hawk now
so you want to fly in planes using software written in Rust
C has the big advantage that having been used for many years, it is very well understood, the compilers that exist are mature, and the formal analysis tools you want to use in a high assurance setting all exist also.
Higher level languages usually have none of these things.
C is probably the least understood language I know of. Vast parts of it are undefined, everyone makes their own decisions and compiler writers define the language.
C is a practical choice because it is performant, legacy code exists, and because a lot of people know the language.
Personally, I would never take a job writing safety-critical code in C. To give a single example of a far superior language for such applications, I would consider SPARK Ada, amongst others. I don't know how people that work on safety critical systems using C can sleep at night.
C is for systems programming where performance is king, not for building software that can kill people.
Nevertheless, the parent was comparing C to Rust, where the language is immature, has no static analysis tools (to pick up the most important bugs), no well defined semantics and is entirely unproven in the field. This is the barrier for entry.
It's absolutely true that Rust is yet to be proven. We need to be ever careful not to oversell its benefits. But here's something that's been proven time and time again: use of C is fraught with horrors and pitfalls, and we should all be frantically seeking to improve the situation; if not via Rust, then via something else.
For example, will the Rust compiler prove that your program must follow some state machine? (SLAM2). Will it compute a useful upper bound on the stack usage for your program? (a3/stack) Will it compute a useful upper bound on the runtime of your program? (a3/WCET) Can one prove (in certain cases) zero potential execution errors? (Astré)? Can one automatically prove generic first order logical specifications of a program? (Caveat)
A lot of these are decades old theory that have been put into practice that simply don't work in the context of a compiler. I'm sure they could be made to work with Rust, but they haven't.
You can do a lot more with static analysis with time and money than you would want to do in a compiler for a language that's a couple of years old.
Furthermore trusting Rust's statically derived guarantees means trusting the Rust compiler to have no bugs. One does not need such a leap of faith for C; they can use a formally verified compiler: http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris...
Writing a formally verified compiler for Rust would be (I'm sure of this) a right pain in the arse.
Part of my zeal is also that Rust's semantics are strictly, er, stricter than C's (disregarding the quagmire of C's undefined behavior), which means that static analysis tools should be even easier to write for it.
Wait, what about autoPilot.js ?
that's a terrifying statement. to those of us who know what a person's first programming projects are like, quality-wise
just terrifying. mindlessly stupid on your management's part
The UI for doors is a little clunky (looks like a win95 app), but it fulfills it's purpose.
Doors equivalent functionality could be built with a web interface and a sql db backend. Maybe any kind of database would work, relational just makes the most sense to me.
That said, assuming DO178B is similar to DO254, it's more about making sure you have a design process and that you are following it, and less about how good that process is.
C is not a good choice when safety is paramount.
"The low-level nature of C and C++ means that bit- and byte-level manipulation of objects is commonplace; the line between mathematical and bit-level operations can often be quite blurry. Wraparound behavior using unsigned integers is legal and well-defined, and there are code idioms that deliberately use it. On the other hand, C and C++ have undefined semantics for signed overflow and shift past bitwidth: operations that are perfectly well-defined in other languages such as Java."
Although IIRC, the impact was limited, because it was quite a feat for a Windows 98 system to stay up for 49 days :)
And it is running 32 bit windows on a 64 bit board.
This seems like a candidate for an automated script that reboots the server every n days or hours. Would such script be considered a potential risk? If so, why?
And there goes the servers because of a stupid script. :-]
Of course they went down anyway and by the far more likely cause of forgetting to reboot.
The result was you typically encountered "jiffy wraparound" after a few minutes of uptime. You learned whether your system was stable in this situation fairly quickly, rather than 248 (or 497) days later. Kernel developers typically don't have uptimes measured in days. Starting the counter close to wraparound increased the likelihood it was going to get code coverage.
There's your answer right there. They write stories for a living, not programs.
Frankly with all the scaremongering going on with computer security these days i kinda agree with Torvalds policy of not highlighting security fixes in Linux patch notes.
They would initiate a controller failover and reboot: https://ma.ttias.be/248-days/
This was a serious problem in some storage systems too: https://www.ibm.com/developerworks/community/blogs/anthonyv/...
From the article it looks like their whole failsafe/redundant system architecture is flawed.
Just like buffer bloat, reboot times and corruptible system state are a chronic systemic flaw in modern technology.
The only stuff that works is the stuff that is used all the time. Look towards crash only software [1] and microreboots [2,3]
[1] https://www.usenix.org/legacy/events/hotos03/tech/full_paper...
[2] https://www.usenix.org/legacy/event/osdi04/tech/full_papers/...
Think Starship Enterprise. You can't turn off the whole ship, or everyone suffocates. You run diagnostics system by system and keep the warp core online as much as possible so you don't run out of power.
It mostly is funny to us, developers, because we have all been trying to convince our bosses that "it will never happen". That object_id being an int4 sequence? You would need one object a second for 70 years to overflow. And yet, somehow, it does, e.g. because someone loaded data with object_id set to 1.9B and the sequence followed from there.
P.S. My favorite pastime? Watching Aircraft Disasters series in an airport. Not brave enough to watch it during the flight yet. Karma might be a bitch and I do not want to test it 10 km up there ;-)
Edit: one theory that seems plausible is that they were "overly paranoid" and put in overflow checks, on a time counter whose overflowing would not have had negative effects otherwise since the other code was designed to handle a wraparound correctly.
int32_t ticks; // 100ths of a second
Although it would be a good engineering choice, a formal verifier would say that:
int64_t ticks; // 100ths of a second
In a hard real time system,
mpz_t ticks; // 100ths of a second, infinite precision libgmp type
The overall lesson from formal methods is that it's impossibly to write formally correct useful programs. So programmers just muddle through.
I would go with uint64_t
as it documents "ticks" as a variable that can not hold negative values and also doubles its range of positive values.
uint64_t ticksOfDuration10ms; // No comment necessary
You'll almost always have a global variable, preprocessor define... or something similar to get the frequency (or time increase per tick), which you should use whenever you have to convert "ticks" to actual physical units. If the actual effective tick rate is visible at many places in your code, both as a symbol name or as a comment, you are most certainly doing something wrong.
(then you'd know it was safe)
int64_t elapsed = (int64_t)(t1 - t0);
if ((t1 - t0) > 50) ...
While it's theoretically possible, using all 64 bits is tricky and very hard to test.
The "can not hold negative values" argument is also weak because a uint does not prevent generating negative values - it only prevents you from knowing that you've generated negative values. Such a state is a bug.
Using a uint only serves to make it harder to test when your system is in an invalid state.
Nothing. Built in arithmetic will do the job nicely.
If the algorithms really depend on an always monotonously increasing tick-counter (which I doubt), the solution is quite easy: After 2^30 ticks set a flag which raises the "service needed" light in the cockpit, taking the plane out of service until it's power cycled. By this you explicitly state that your device cannot be used longer than 120 days continuously.
Then the simple "raise service-needed signal" would be a valid workaround and easily testable local change for the next two years until the extensively fixed-algorithm went through testing and certification.
What made this bug dangerous is that nobody knew about it, that's the main problem that needs to be solved.
uint32_t t1 = ...;
uint32_t t2 = ...;
if ((uint32_t)(t2 - t1) >= UINT32_C(0x80000000)) {
// t2 is before t1
} else {
// t2 is after or equal to t1
}
For example you time events at a fixed time interval, and it will keep going forever in spite of clock roll-over.
uint32_t next_time = now();
while (1) {
while ((uint32_t)(now() - next_time) >= UINT32_C(0x80000000));
printf("Shoot\n");
next_time += interval;
}
but I would suspect Boeing used something better than C.
Invariably, cost. SPARK Ada is demonstrably superior to C for safety-critical development (I can't cite the sources for this, but a major company developing safety-critical software has shown this to be the case).
But, SPARK Ada requires a lot of highly skilled manpower and it's slow to develop. C gets the job done, albeit with lots of bugs.
Realistically, it seems to me that avionics etc. will be written in C for a very long time to come. It all comes down to the cost and availability of programmers.
This is a scary-ass bug in a codebase that was supposed to be authored to strict professional standards.
http://lxr.free-electrons.com/source/include/linux/jiffies.h...
(Learn from history. Don't cling so hard to the notion that your language will make you into super-programmers. Certainly, some tools are better in certain contexts than others. However, group culture and the quality of working relationships often have an effect even greater than choice of language. Besides, people often dislike someone who projects an air of superiority.)
For example, incorrectly using a X > Y comparison on values that are congruential (and do not overflow) isn't an "overflow bug". You can only locally compare values that are close together on the wheel, using subtraction.
The simple thing to do with tick counts is to start them at some high value that is only minutes away from rolling around. Then the situation reproduces soon after startup, rather than days or months later, and its effects are more likely to get caught in testing.
Treat all the ones and zeros correctly and everything else takes care of itself.
Wonder how long it could take for the update to be actually available (after testing, approving, ...). Are we talking weeks, months, years?
[1] https://s3.amazonaws.com/public-inspection.federalregister.g...
My suspicion is the "Reboot" approach is pretty common to aviation systems. It wouldn't surprise me that many of the components are rebooted daily, and almost certainly on a weekly basis.
120+ days without a reboot sounds unlikely to me.
However, since there are so many electricly operated systems, you really need power. The B787 as is No Bleed [1], so electrical power is also used to pressurize it [2]. Need Electric Power.
[1] http://www.boeing.com/commercial/aeromagazine/articles/qtr_4... [2] http://www.airliners.net/aviation-forums/tech_ops/read.main/...
That's the power that I was talking about requiring a reboot. Not sure if it's related to the AC power associated with the bug in question - possible there are two AC power systems on the plane?
[1] http://www.reuters.com/article/2014/02/04/us-poland-dreamlin...
As much as we'd like plane manufacturers to test things to death, it'd become too expensive too quickly. For all we know, this software could be written by a contractor, or the firmware for a third party part.
As far as I know, N-version programming was effective when software systems were small (shuttle ran on 50k lines of code) and where poring over every single line was possible, because the hard part was coming up with the spec.
Nowadays a big plane like the A380 might be expected to have 100M lines of code in its subsystems, and it's simply too expensive.
Why does an airplane require 100M lines of code?
Multiply by all the little and big subsystems, the embedded chips, in-flight entertainment, network gear... 100m SLOC is too low, I think.
where it states that the airbus A380 has more than 100 million lines of code in its avionics systems.
Do these systems not have hard real-time requirements about the execution time and periodicity of tasks which can't be guaranteed by the time-sharing scheduling algorithms in Linux?
It's all about the latency guarantees and that means that you're going to have to inspect each and every path through the code for length. With the complexity of the linux kernel that's a pretty tough job and I suspect that anything lower than a few hundred milliseconds (guaranteed!) is out of the question.
I built a little controller using linux that required hard real time during a long (multiple minutes) of operation and the way I hacked it was to simply disable all interrupts and recover the various drivers as good as possible once that phase was over. It worked well but was mostly deaf to input during that time except for polling one 'stop' switch which would cause the machinery to coast down to a halt after which interrupts would be enabled.
Good enough for tinkering but I certainly would not bet anything in production on that strategy.
Real time is hard, soft real time is hard enough (without guarantees but with a best effort and a very large fraction of the deadlines satisfied), hard real time (no misses at all, guaranteed) is hard for a kernel of any complexity.
They'll definitely build a prototype using Linux but they won't get that certified so it literally 'won't fly', it's just a means to speed up initial development.
Small enough that I could-reimplement it in approximately 3500 lines of code + another 850 for the virtual memory management.
This could only work if the entity paying for the certification had a way of making that money back somehow and I don't see how that could be done.
It would cost a significant amount of money to develop the necessary artifacts and engage the FAA to obtain a certification.
What I think the whole thread above misses is that the economics simply aren't there, cost isn't the limiting factor for the OS licenses for avionics but an extra certification track (especially for a fast moving target) would be, besides, it is not just the OS that gets certified but you will also have to (separately) certify (usually) the hardware that it runs on (unless you're going to use a design that has already been certified).
That means that modifications are expensive and that 'known to be good' trumps 'could be better' or 'could be cheaper in the longer term'.
Someone would have to come up with a very good reason to see open source trump the existing closed source solutions.
In addition, a modular microkernel architecture could use reproducible builds to generate identical binaries from identical source. This would enable binary components to be certified both separately (akin to unit testing) and as an integrated system (mix and match components). This could reduce overall duplication and certification costs, even among competing commercial products derived from seL4 components.
They should be able to keep it under 10M lines pretty easily if they actually cared about bloat.
Think GCC 5 is about 15 million or so now.
Or compare to the Apollo missions and the space shuttle being well under a million.
I'm not saying that it would be easy to redo the entire system from scratch now, I'm just saying that if it was a design goal from the start it wouldn't have been very onerous.
All of these things just add more and more code.
For all we know, if the spec required a counter of 100ms intervals, all N implementations could contain the same bug.
N-version avoids random, but not systematic bugs.
(P.S. the link to the pull request in the bug tracker is wrong, because the repo was once deleted and re-created, losing all the old pull requests).
It's a terrible oversight, and makes me wonder about the rest of the code, but are there very many airliners that are online for that long at once? I don't know much about how commercial air travel works behind the scenes.
Does anyone know the impetus behind the study?