Categories
C standard programming languages software security

C is not a serious programming language

The C Standards process over the last few decades has addressed both optimization and pointer type safety largely through a concept called “undefined behavior”.  The idea is that instead of  positive rules for what compilers and programmers can do, the Standard will identify some program behavior as something compilers can interpret how they want — really without any guidance at all. These things are not syntax errors that must cause the compiler to reject code or even, necessarily things the compiler must warn about, but are instances of behavior that are outside the standard. It is not even clear whether “undefined behavior” is erroneous at all or even avoidable.  I think this whole process is due to a misreading of the C89 standard, but more importantly, it’s sloppy, makes it hard for programmers to have an intuition about the language, and leads to paradoxical results or nasty surprises.  For example, writing a value to a  variable from a pointer that has been advanced past the end of the object it was supposed to point to has been sort-of-kind-of designated as “undefined behavior”. Here’s  an example: the output of a simple C program compiled and “optimized” by gcc 11

pointer1 = 0x404039 pointer2=0x404039 they are not equal

They look equal, don’t they? Clang 12, on the same code uses  normal arithmetic to compare numbers.

pointer1 = 0x404039 pointer2=0x404039 they are equal

An earlier version of gcc, gcc 4.8.3 also knew how to compare numbers:

pointer1 = 0x404039 pointer2=0x404039 they are equal

And Gcc 11 again, but this time with the optimizer turned off (-O0):

pointer1 = 0x40403a pointer2=0x40403a they are equal

Here’s the code ( see NOTE1 in the code )

#include <stdint.h>
#include <stdio.h>

typedef char T;
T p[1], q[1] = {0};
int main(){
        T *ip = (p-1);//NOTE1. change +1 to -1 if gcc -O0
        T *iq = q;
        printf("pointer1 = %p pointer2=%p ",ip,iq);
        if (iq == ip) {
              printf("they are equal");
             }else printf("they are not equal\n");
}

The explanation is that gcc notices that ip has been set to a fishy address

:6:8: warning: array subscript -1 is outside array bounds of 'T[1]' {aka 'char[1]'} [-Warray-bounds]
6 | T *ip = (p-1);//add if gcc -O0
|  ^~

and, gcc 12 helpfully “optimizes” on the basis of “ip”  holding an “invalid” address, perhaps reasoning that the two pointers “cannot” be equal. Under the prevailing interpretation of the C Standard, compilers can assume “undefined behavior” cannot happen, even if they generate code that makes it happen  At least, in this case, there is a warning, but often these “optimizations” are silent. The rationale is that programmers should not be messing about looking at the order of variables in memory (even though that’s not unusual in C) and that compilers should be able to optimize under the assumption that pointer arithmetic does not ever steer a pointer between objects.  To be fair, most of the time that a pointer goes beyond the boundary of an array, it is an error.

Here’s the link on Compiler Explorer. The example is modified from one given in a post by  Ralf Jung  who attributes it to Chung-Kil Hur (I’m sure both disagree with my reaction).

If C was a new programming language, you might decide that the %p output should provide the address and some additional data.

pointer1 = 0x404039 (int) pointer2=0x404039 (int, invalid)  they are not equal

That would make some sense. But in this case, you’d also have to think through all the implications of this design decision, which nobody has done (see below).  For example, since the 1990s, C Standard has made it impossible to write memory allocators in conforming C. Suppose we have a network application that is performance constrained by “malloc” and we want to put a caching allocator for small and jumbo packets on top of malloc:

(small_packet_t *)newsmall();  (large_packet_t *)newjumbo();  freepacket(void *);

The idea is that when either allocator has too little memory, it calls malloc (or something else) to get a big chunk of memory, puts it into a list of free storage, and slices it up when it is asked to allocate. Maybe something like

free_block_t *p; …. p =malloc(K); p->size = K; p->next = Head; Head = p;

But according to the sloppy type rules in the Standard, after writing through a “free_block_t” pointer, that block now has “effective type”  of “free_block_t” and if we allocate part of it to a caller that then writes to it as a small_packet_t, the behavior is undefined and all bets are off because we have tried to store a value to an object with a different effective type. Even worse, imagine that “freepacket” tries to merge freed packets into blocks again! Suppose 4 small packets can be freed and then consolidated and allocated as a single jumbo packet.  Nope. No can do.  Once storage has an effective type, it is frozen to that type.  How does malloc/free work then? Oh, easy, it is special cased in the standard. Similarly, there is a special case for char pointers so that memcpy can be implemented, even if not very efficiently. To get other allocators to work, C programmers rely on “opaque” interfaces. If the allocators are in a separate file, and we do not have link time optimizers, then probably the compilers won’t be able to learn that the type rules are being violated. But then as link time optimization (LTO) comes in, the whole thing may silently be “optimized” to fail.   One of the other ridiculous  properties of the undefined behavior rules is that they are unstable or ephemeral and depend on the current capabilities of the compiler to see through opaque interfaces or otherwise figure out about some particular instance of undefined behavior.  That is, the rule is something like: “this will work as expected until the compiler figures out that it is undefined behavior”. As you can see above, gcc learned to recognize the undefined behavior somewhere between versions 4.8 and 11 and still can’t figure it out at lower levels of optimization.

Here’s another “optimization” from Clang-C

int are_we_out_of_memory(void) {
        int *y = malloc(2);
        return y == (int*)NULL;
}

Under -O3 optimization, this always returns 0 in Clang-C. Why?  Perhaps in this case Clang is reasoning that the pointer becomes invalid when the function returns because the storage, if any, returned by malloc is now inaccessible, so the comparison is invalid. Who knows? Optimization is easier if we don’t have to care about correctness.

Here’s a question  I asked some compiler and standards developers: can the compiler assume “b” is false and delete the whole branch?

int getadata(int b, char *buf, int n){
       int *p; //forget to initialize
       if(b){
           read(0,buf,n);
           *p =0;
       }
       return 1;
}

Since p is uninitialized, the compiler may decide the assignment, which is “undefined behavior” can’t happen, so the whole branch can be assumed away – and this reasoning would apply no matter what else we do inside the branch. So the code that calls “getdata(1,buff, 1000)” over and over will get nothing done and might even itself be “optimized” away.  Imagine:

char *buf = malloc(1000); getdata(1,buf,1000); if(buf[23]== 'x'){ ....}

 

On the basis of the first “optimization”, the compiler may see that the “if” depends on reading uninitialized memory and delete that case too. With a low level of optimization, the compiler may generate those reads and then silently delete on a higher level of analysis – and different C compilers can make different choices. Effectively, programmers have to guess.

Here is a hypothetical case:

char *b,good;
n = read(fd,b,m);
good = b[m-1];// undefined if n < m
if(n == m  )dosomething(good);
else badread(good);//can we delete this case

Right now, code  like this will compile as expected. But that’s only because the compilers do not incorporate knowledge about “read”. Suppose the compiler understands that if n != m, then b[m-1] is uninitialized and deletes the badread case, because otherwise “good” is the result of reading uninitialized memory which “can’t happen”? So this code may work, contingent on the compilers not figuring out what “read” does.

There is right now in the C Standards process an effort to incorporate pointer “provenance” so that compilers are permitted to consider pointers as pairs (provenance, abstract address) and an 80 page proposal that appears to have a lot of support.  You can read some of the ongoing discussion about this proposal in the message archive. One of the interesting things about this proposal, in the current state, is that it doesn’t provide any solution to the malloc issue – but suggests some solution should be found.  Similarly, it doesn’t discuss how mmap can work with the proposal. The proposal text is also ambivalent about how == should work for pointers. Why? Because it’s impossible for compilers to always correctly figure out the provenance of a pointer, however the proposers want the compilers to enforce provenance rules when they can. Programmers are supposed to just figure it out.

 

See also the purpose of C.

 

Categories
software security

Right to private jet ski use while collecting disability

New York authorities said the warrants led to the indictments of firefighters, police officers, and civil servants on disability fraud charges. The Facebook data, which included user photos and videos, showed employees who claimed they were disabled performing a variety of activities, including fishing, martial arts, and even jet ski riding. – Ars Technica

Categories
software security

Droning on about computer security

Good grief.

The US military’s unmanned Predator and Reaper drones are continuing to fly remote missions overseas despite a computer virus that has infected their US-based cockpits.
Government officials are still investigating whether the virus is benign, and how it managed to infect the heavily protected computer systems at Creech Air Force Base in Nevada, where US military pilots remotely fly the planes on their missions over Iraq, Afghanistan and elsewhere.
“Something is going on, but it has not had any impact on the missions overseas,” said a source, who was not authorized to speak publicly.
Armed tactical unmanned planes have become an increasingly valuable tool used by the US military to track and attack individuals and small groups overseas, but the virus underscores the vulnerability of such systems to attacks on the computer networks used to fly them from great distances.
Rob Densmore, former US navy airman, told Al Jazeera that the infection was a common keystroke logging virus – which registers the keystrokes pilots use to control the unmanned drones from afar.
“It has to have a point of access, so we know that thumb drives – basically USB drives – are used to upload navigational information, guidance information to Predator and Reaper drones.
“And if there’s a way somehow that that information, or that thumb drive, can come into contact with a network or with the internet, that’s where the danger is because that basically means that information can be carried across from the Reaper drones.”

http://english.aljazeera.net/news/americas/2011/10/201110816388104988.html

Government approach to security can be described as designing an unsinkable boat that has no doors between compartments and then, to make it usable, cutting a random and increasing number of undocumented holes between compartments.

 

Categories
software security

Security news

The lesson of this story is that even (particularly?) computer security companies cannot put up with the inconvenience of standard security precautions.

Greg Hoglund’s nightmare began on Super Bowl Sunday. On Feb. 6 the high-tech entrepreneur was sitting in his home office, trying to get to the bottom of some unusual traffic he was seeing on the Internet. Two days earlier he’d noticed troubling activity hitting the website of HBGary Federal, the Sacramento startup he helped launch in 2009. He suspected some kind of hacker assault and had spent the weekend helping to shore up the company’s systems. A few hours before Green Bay kicked off to Pittsburgh, Hoglund logged into his corporate account on Google (GOOG)—and confirmed his fears.

He couldn’t get in. Someone had changed the password and locked him out of his own e-mail system.

He used Google mail – and several people had the administrator password.

Categories
software security

Security for dummies – a lesson for smart grid

WASHINGTON — Militants in Iraq have used $26 off-the-shelf software to intercept live video feeds from U.S. Predator drones, potentially providing them with information they need to evade or monitor U.S. military operations.

Senior defense and intelligence officials said Iranian-backed insurgents intercepted the video feeds by taking advantage of an unprotected communications link in some of the remotely flown planes’ systems. Shiite fighters in Iraq used software programs such as SkyGrabber — available for as little as $25.95 on the Internet — to regularly capture drone video feeds, according to a person familiar with reports on the matter.

So what are the lessons. First, “security by obscurity” is equivalent to “hope is a plan”

The potential drone vulnerability lies in an unencrypted downlink between the unmanned craft and ground control. The U.S. government has known about the flaw since the U.S. campaign in Bosnia in the 1990s, current and former officials said. But the Pentagon assumed local adversaries wouldn’t know how to exploit it, the officials said.

Whoops!

And second : use standard protocols

Predator drones are built by General Atomics Aeronautical Systems Inc. of San Diego. Some of its communications technology is proprietary, so widely used encryption systems aren’t readily compatible, said people familiar with the matter.

Categories
operating systems software security systems

Deterministic multithreading

An interesting paper appearing in ASPLOS proceedings provides a “deterministic” locking method

Kendo enforces a deterministic interleaving of lock acquisitions and specially declared non-protected reads through a novel dynamically load-balanced deterministic scheduling algorithm. The algorithm tracks the progress of each thread using performance counters to construct a deterministic logical time that is used to compute an interleaving of shared data accesses that is both deterministic and provides good load balancing. Kendo can run on today’s commodity hardware while incurring only a modest performance cost ( http://www.gigascale.org/pubs/1883/asplos073-olszewski.pdf)

There is similarly motivated work on Java going on at UIC: http://dpj.cs.uiuc.edu/DPJ/Home.html

Both works refer to Lee’s paper which I discussed earlier. Nondeterministic threading is a  historical accident in computer engineering. Operating systems introduced time-sharing methods so single thread programs could be run in parallel during I/O delays and then so that multiple users could reasonably fairly share a processor and then so the OS and service programs could provide multiple services to a user at the price of slowing down user applications.  Exposing this system to users has been a mixed blessing. Certainly in the controls world, non-determinism is a dangerous fault.

Categories
software security

Marine One Blueprints via Pirates Bay

Goodness. The US blueprints for Marine1 show up in Iran.

“What appears to be a defense contractor in Bethesda, Md., had a file-sharing program on one of their systems that also contained highly sensitive blueprints for Marine One,” Boback said.

Tiversa also found sensitive financial information about the cost of the helicopter on that same computer, WPXI-TV reported.

Categories
software security

Mobile device security and President Obama

Obama’s fighting hard to keep his Blackberry

President Barack Obama will have a beloved BlackBerry — and maybe a second, more secure smartphone-like device — with him in the White House.

The president has been adamant about continuing to use a BlackBerry, a smartphone with Internet and e-mail access, despite concerns that are likely making the National Security Agency as nervous as the Secret Service on Inauguration Day when Obama left his presidential limo twice to walk and wave to crowds along Pennsylvania Avenue. MSNBC

Categories
software security

Updated Dijkstra vs Perlis (really, DeMillo)

See below.

Categories
academics software security theory

Dijkstra versus Perlis (updated)

Bertrand Russell.
Bertrand Russell.

Dijkstra wrote:

He [Perlis] published a very obnoxious paper arguing against a mathematical approach to programming cite

The paper  by De Millo, Lipton and Perlis  starts as follows:

Many people have argued that computer programming should strive to become more like mathematics. Maybe so, but not in the way they seem to think. The aim of program verification, an attempt to make programming more mathematics-like, is to increase dramatically one’s confidence in the correct functioning of a piece of software, and the device that verifiers use to achieve this goal is a long chain of formal, deductive logic. In mathematics, the aim is to increase one’s confidence in the correctness of a theorem, and it’s true that one of the devices mathematicians could in theory use to achieve this goal is a long chain of formal logic. But in fact they don’t. What they use is a proof, a very different animal. Nor does the proof settle the matter; contrary to what its name suggests, a proof is only one step in the direction of confidence. We believe that, in the end, it is a social process that determines whether mathematicians feel confident about a theorem–and we believe that, because no comparable social process can take place among program verifiers, program verification is bound to fail.

To me, the problem with Dijkstra is that he was so sharp and such a good writer that he was able to make persuasive cases out of obviously wrong ideas. Dijkstra wanted to be a scientist in the model of theoretical physics, not an engineer. I’m pretty confident that Dijkstra was wrong: programming is engineering – in fact, physics is not as far from engineering as some people would like to believe. I’m not a huge fan of the engineering discipline as it exists in the USA. It has all sorts of negative aspects – including those Dijkstra railed against. But the vision of a programmer as, not a mathematician, but a formal logician flying far above the grubby compromises and trade-offs of mere engineering in a platonic bubble of pure reasoning is wrongheaded.

Dijkstra published some criticism of the Demillo paper at the time and in their response the authors stated something that, as far as I know, remains true

We must begin by refusing to concede that our confidence in a piece of real software has ever been increased by a proof of its correctness

When I was in graduate school (a long time ago), a famous formal methods sctandem_mugholar came for a talk and explained to us that formal methods were needed if we were ever going to develop fault tolerant software. I pointed out that, for example, the Tandem Software worked pretty well in practice. “It cannot”, retorted the famous scholar.

So there.

Here’s Edsger Dijkstra discussing the birth of the use of axiomatics in computer science – the start of “formal methods” research.  What’s striking is the assumed choice between “axiomatic” and “mechanistic” as if there was no other way. In a later note he writes:

And now we are back at our old dilemma. Either we take by definition all properties of the model as relevant, or we specify in one way or another which of its properties are the relevant ones. In the first case we have failed to introduce in the name of “divide et impera” an interface that would allow us to divide and rule and the study of how we could build upon the (only implicitly defined) interface seems bound to deteriorate into a study of the model itself; in the second case we are again close to the axiomatic method….

[…]

Or, to put it in another way: if the traditional automata theory tends to make us insensitive to the role interfaces could and should play in coping with complex designs, should it then (continue to) occupy a central position in computing science curricula?

And I’m struck by the idea  that seems utterly wrong to me, that one either uses the methods of formal logic OR one is stuck without any ability to abstract or underspecify,  And it’s also interesting to see this impoverished view of automata theory that underpins so much of the formal methods literature.

The reason mathematics has advanced so much was not because of the Euclidean axioms-lemma-theorem straitjacket, but in spite of it. Luckily, when we actually discover mathematics, we do it the Babylonian way, empirically and algorithmically. It is only when it is time to present it, that we put on the stifling Greek formal attire.

so says Doron Zeilberger

 

Updated:  with minor format improvements 2/16/2016 and merged with an earlier article 10.2.2016 Erev RH.