The Apple iMessage bug

Wayne,

I’m back in Tampa after my sweet honeymoon with my darling new wife, Linnea. We spent a week in my home town, Washington, DC, where she had never been.

Now back to my task of asking you tough questions and learning from your answers.

Ben Linders interviewed you for InfoQ on the subject of provably correct software on May 22, 2015.

You were articulate and clear. Obviously you have been thinking about the many problems of software engineering that arise from the difficulty of writing bug-free code and producing bug-free products and systems. Since many smart engineers and researchers have been thinking about this for decades, it is remarkable, I think, that we still read of bugs in crucial, widely used software produced by, we suppose, the best engineering talent available.

I’d like to ask you to consider the remarkable bug recently uncovered in some Apple products that became known at about the time your interview appeared. 

Here’s a description of the problem. There are many other articles about this bug. I’ll summarize the problem, as I understand it, as follows: Someone sends you a text message with a precise and particular string of characters, including some specific ones in Arabic (!). When you open the message to read it, the system’s attempt to display the character sting crashes the operating system. Indeed, the damage is so great that it is difficult to restore the operating system properly.

Evidently, this afflicts iOS in iPads, iPhone, and Apple Watches. Of course, no one is likely to receive this message, and in that sense, this is not exactly a serious bug. But what other obscure patterns of symbols might do this?

My question to you is whether the methods of formal correctness proofs and other aspects of meta-analysis of code and applications could locate such a bug? Since Apple’s engineers are among the best, why would they have failed to find a bug that can crash their operating system, if solid and effective methods such as those you describe are available?

Bernard

3 Comments

Filed under Software

3 responses to “The Apple iMessage bug

  1. Bernard,

    Many different things could have caused the Arabic-character Apple iOS messaging crash. I haven’t read recent posts about the crash, so all of what I write here is uninformed speculation. I do however have some experience with rendering Unicode characters, though not in Arabic.

    If Arabic is relatively new to iOS or new to this app, then the first place I’d look is in the right-to-left rendering of composite Arabic characters. Easy to get something wrong when you’re programming in reverse, so to speak, such as doing an increment where a decrement should have been.

    I think it’s unlikely the crash comes from imperfect communications or management of state when the message arrives and is being prepared for rendering; if I’m right on this, then the kind of modeling and formal proof I advocate would not have found it.

    In sum, I suspect that the crash is an edge case in rendering of sequences of composite right-to-left characters, and that Apple’s automated testing didn’t happen to uncover this exact case. They can’t possible feed all possible strings during testing, only representative ones. I believe Apple will find the problem and fix it soon. As you say, though, it’s not really urgent, just newsworthy.

    In my experience, people today accept all kinds of bugs in iPhones, iPads, Android devices etc given how useful and valuable these devices are and how fast they evolve. As we’ve always done with computers, when a device crashes, power it down and back up and get on with life. The problem mostly doesn’t happen again. If a crash happens, however, in a safety-critical auto control module or medical device, it can’t just be shrugged off with a reboot. We are absolutely obligated to apply every available tool, within reason, to prevent such devices from crashing in actual use. Apple is not obligated to use all available tools to fortify their devices unless the devices become integral to larger safety-critical systems.

    Wayne

    Like

    • bleikind

      Wayne,

      You speculate that the Apple iMessage bug might be an off by one or picket fence error. This seems a good guess to me. It seems, therefore, that even though an engineer might have formally proved that her code is correct, it would still have common bugs in it.
      I wonder what types of problems formal methods find? What problems will formal proofs of correct coding fail to find?
      Indeed, in view of various issues, such as the stopping problem, I’d guess that there are limitations the assurances that formal methods can provide an engineer.
      Now some types of errors in programming arise because of human weaknesses of memory or attention. The modern versions of programming and development systems have made impressive strides using the computer’s strengths to help humans overcome their weaknesses. I wonder that their doesn’t seem to be something built in to help us with off by one or picket fence errors.
      Bernard

      Like

  2. Bernard,

    In a few words, based on an article referenced below as well as on other sources, formal methods would not have found this bug but commercial static analyzers could have. Details follow.

    Formal methods of the kind I work with exhaustively test all execution paths through a MODEL of communications and state management among a set of components in multiple threads and/or multiple processes. These formal methods find unhandled events, disallowed events, race conditions, deadlocks, etc. Other kinds of formal methods test MODELs for what are called liveness, safety and fairness properties. Liveness: will execution eventually reach some desirable state, such as normal termination? Safety: will some undesirable state never be reached, such as two trains on the same small zsof track at the same time? Fairness: Will a certain desirable action always occur again eventually? Formal methods concentrate on the fundamental logic of software by abstracting away from bits and bytes into components, interfaces and execution paths. When a formal method finds a logic flaw, the developer must fix it in the model and then either automatically regenerate source code from the model, or fix the problem manually in source code that is not automatically generated.

    Static analyzers comprise a completely different set of reliability tools. Some leading commercial ones are Codesonar, Coverity, Klocwork and Parasoft. These tools operate on source code, not on models. They check that coding standards have been followed, and more importantly they uncover a wide range of bugs including buffer overflows, memory access violations, null pointer references, and many more.

    According to this article from 2013, http://www.theregister.co.uk/2013/09/04/unicode_of_death_crash/, the Apple iOS Arabic text crashes are due to memory access violations that come from wrongly calculating string lengths in complex Unicode sequences like those found in Cyrillic mixed randomly with Arabic.Static analyzers can and will trap such bugs and guide developers to a fix, but usually only if fed test sequences that cause the bug. The article says that the guilty strings are nonsense and would never occur in any real-world use case, thus it’s unlikely that typical test suites used by Apple prior to shipment would have fed them to the software. If the application were safety-critical, then the vendor would be obligated to test far more exhaustively than Apple probably did, including nonsense sequences.

    There is no such thing as a 100% safe or 100% reliable software-controlled system. One cosmic ray can flip a bit in a 2005 Toyota Camry’s engine control module’s memory and cause runaway unintended acceleration. Formal methods and static analyzers only help reduce risk to acceptable levels. Builders of safety- and business-critical software are morally and legally obligated – or should be – to use available formal methods and analyzers on their products.

    Hope this clarifies…

    Wayne

    Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s