Slashdot Mirror

Pardon my ignorant question, but how is it a problem to have traction control? Wouldn't it be enough to glue traction strips to the feet or something?

That's like wearing shoes with golf spikes all the time.

Traction control for feet does roughly the same thing as automotive traction control for cars. The basic idea is to keep the sideways force below the break-loose point. This is the down force on the wheel times the coefficient of friction.

For car wheels, the down force is mostly constant. For a legged robot, it changes throughout the ground contact phase So the side force has to be actively controlled and changed throughout the ground contact. It's also necessary to compensate for leg angle.

Legs have an additional option. If a leg has three joints, you can adjust the angle at which the contact force is applied. This is a big win on hills.

I used to work on this stuff in the mid-1990s, but nobody was interested in building legged robots back then. It could be used for animation, but it was overkill for games. I never expected that DARPA would spend $120 million on BigDog. Robotics projects in the 1990s were tiny.

Been there, done that, 30 years ago.

Every Windows driver with WHDL certification has passed the Microsoft Static Driver Verifier, which is a proof of correctness checker. Passing means that the driver won't blow away the rest of the OS with a bad pointer, subscript error, or other fatal error. Since Microsoft started requring this in Windows 7, Windows OS crashes have been way down.

About 5% of verifications either require too much time or too much memory. Any formally undecidable program would hit one of those limits. If it's that hard to tell if a driver has a bug, they assume the driver has a bug.

So there. Solved problem in practice.

This is C code, the only major language that doesn't know how big its arrays are. After 30 years of buffer overflow bugs, you'd thing we'd have something better now for low-level programming. The higher level stuff, where you can use garbage collection, is in good shape, with Java, C#, Python, etc. resistant to buffer overflow problems. C and C++, though, are still broken. C++ tries to paper over the problem with templates, but the mold (raw pointers) keeps seeping through the wallpaper.

I've tried. Here's my paper on a stricter version of C that's object-compatible with existing C code. It's techncally possible to fix this problem. The political problems are huge.

The problem is C. Programs in all the languages that understand array size, (Pascal, Modula, Ada, Go, Erlang, Eiffel, Haskell, and all the scripting languages) don't have buffer overflow problems.

It's not an overhead problem. That was solved decades ago; compilers can optimize out most subscript checks within inner loops.

I've proposed a way to retrofit array size info to C, but it's a big change to sell. There are many C programmers who think they're so good they don't need subscript checks. Experience demonstrates they are wrong.

The code:

for ( i = 0; v3 != '\n'; ++v2) // Dangerous loop, copying data to a stack buffer, until an end of line is found
{ if ( v3 == '\r' ) break;
*(_BYTE *)(i + a1) = v3; // Byte copy to the stack, without having destination size into account.
v3 = *(_BYTE *)(v2 + 1);
++i;
}

The company that let that code out the door should be sued for gross negligence, and managers fired. That's not the only example; they failed to do basic checks at least three times. This isn't a subtle bug. This is failing C Programming 101.

(Several times, I've tried to convince the C standards committee to put a "strict mode" in the language and move towards a form of C that's resistant to buffer overflow problems. Maybe I should try again.)

C - now with over thirty years of buffer overflows.

My obvious password detector, published in 1984

I came across this password strength detector the other day. It really cheered me up, as it uses a scientifically-justifiable approach (information entropy FTW!) and it laughs in the face of a number of tricks that many people recommend despite them being actually weak (replacing "o" with "0" only really adds one bit of security, which is nearly nothing, whereas adding another word adds far more despite being easier to remember).

Sigh. My obvious password detector, published in 1984:

The algorithm used requires that the length of the password be within configurable length limits, and that the password not have triplet statistics similar to those associated with words in the English language. This is an inversion of a technique used to find spelling errors without a full dictionary. No word in the UNIX spelling dictionary will pass this algorithm.

Users should be advised to pick a password composed of random letters and numbers. Eight randomly chosen letters will pass the algorithm over 95% of the time. A word prefaced by a digit will not pass the algorithm, although a word with a digit in the middle usually will. Two words run together will often pass.

(The code linked is the original version in pre-ANSI C. Yes, kiddies, that's what C code once looked like.)

It's written in C and it's a buffer overflow exploit, right?

We warned you. You didn't listen. Now suffer.

Regarding C/C++, Those languages are optimized to be close to the hardware; that's their forte: they are semi-assembler-language. If you optimize the language for software engineering improvements (code design & reliability), then you likely de-optimize it for hardware.

This is a common, and dangerous, misconception. It's quite possible to have efficient languages that are close to the hardware without having buffer overflows all over the place. Pascal did it. The various Modulas did it. Ada does it. Go is getting close. Subscript checking is really cheap, and often free, if the compiler understands how to optimize it. Hoisting subscript checks out of loops is important. The current Go compiler gets the easy cases (FOR loops), which is enough to keep the overhead down for inner math loops. (Math inner loops in Go would optimize better if it had real multidimensional arrays. That may happen.)

We don't have many good alternatives. Hard-compiling Java to machine code (which GCC can do) never caught on. The Modula family died with DEC. Ada was just too wordy. C is fixable, as I point out occasionally, but that's never going to happen short of a 9/11 sized event caused by insecure software. Garbage collected languages are unsuited for low-level programming, although they can go fast.

C++ was supposed to fix C, but the C++ committee went off into template la-la land, and overcomplicated the language.

Address space randomization is security through obscurity. It's an admission that you can't fix your buffer overflows. It slows down attackers, but there are counters, such as "spraying attacks".

Worse, it means that bugs become nonrepeatable and harder to fix. So software quality degrades. It produces more of those errors you see in bug tracker as "Closed - can't reproduce".

This is a fixable problem. Microsoft could use C#, or Java, or Go, or Python, or Javascript - languages with subscript checking. Or fix C. Or extend their static driver verifier to cover more kinds of code. Address space randomization just obscures the problem.

It's not clear whether he grew dumber or smarter, but he certainly made the transition from respected engineer to patent troll effectively enough.

The problem remains the C language. C (and C++) is the only remaining major language prone to buffer overflows.

This can be fixed. See "Safe arrays and pointers for C through compatible additions to the language". This is a proposal for a "strict mode" for C which prevents buffer overflows. It's been discussed on Lambda the Ultimate, the C standard newsgroup, and the GCC development list, and with each round of criticisms, the design is tightened up.

This proposal includes a "strict mode", in which the rules are tighter, and ways to talk about the size of arrays. Non-strict code can call strict code, and vice versa. So there's a gentle migration path to all-strict programs, one source file at a time. It's an extension to C, not a new language. Some of the necessary features for this are already in C99 or are GCC extensions, so I'm trying to get this into GCC as an extension so it can be tried in the real world.

It's no longer acceptable to say that this problem can't be solved. It can. It just takes the will to solve it. Prodding from the security community will help.

Strict code is mostly about declarations. For example, the Linux "read" function, which is now declared int read(int fd, void* buf, size_t len); would be declared int read(size_t len; int fd, void_space (buf&)[len], size_t len); Instead of passing a pointer, you pass a reference to an array, a reference with an associated size. So the language knows how big the array is. Incidentally, the first "size_t len;" is a forward declaration of len. That's an existing but rarely used GCC extension. It's needed because so many C, UNIX, Linux, and POSIX APIs have the buffer param before the buffer size.

(For those few of you who know what a C99 variable length array parameter is, you'll wonder why this syntax differs from that. It's a long story. C99 VLA params are demoted to pointers at function entrance, losing the size info. It turns out nobody uses C99 VLA params; repeated searches have failed to find any of them in open source code. Also, Microsoft refused to implement them in Visual C/C++, they're incompatible with C++, and they've been demoted to an optional feature in the latest C standard draft.)

Worked that out back in 1995. See this the "running on rough terrain video. Watch at 1:40.

The next step, which the U. Penn people don't seem to have taken yet, is to solve this as a two-point boundary value problem. Then, instead of trying to maintain attitude during flight, you try to land at a specific time in a specific place with a specific attitude.

Doing that is rocket science. Rocket science is about control of underactuated systems, where the control system has fewer actuators than there are degrees of freedom to be controlled. You want to reach a specified point at a specified time at a specified velocity in a specified attitude. All you have available is the ability to thrust in one direction and to change attitude slowly. But this problem is solveable and there are known solutions. Applying that to robots leads to gymnastics.

The quadrotor people are already doing this kind of thing, but it hasn't been done much for legged machines yet.

The intent of the new syntax is that &char[n] buf means passing a reference to an array of size n. char[n] is an array type, something C currently lacks. Syntax like this is needed so that you can have casts to array types.

I've had a few go-rounds at this syntax problem. See "Strict pointers for C". Unfortunately, there's no solution that's backwards-compatible with existing code. However, mixing files of old-style and new-style code is possible, and mechanical conversion of old-style code to new-style code looks possible.

It's worth looking at this again now that C's market share is back above that of C++.

I proposed, back in 2000, that Microsoft be required to provide a full warranty on their products as part of their antitrust remedy. "Full warranty" has specific meaning in US law; see the article. A few vendors have provided full warranties and not found it too expensive. Notably, GTech, which builds gambling systems, is held financially responsible for errors made by those systems. This costs GTech less than half of one percent of their revenue.

It's time for the computer industry to grow up and take on warranty responsibilities. The auto industry had that forced on them by Congress in the 1960, over the screams of the auto industry. Cars rapidly became safer and more reliable.

I wrote "Safer arrays for C" back in 2008. After working on this for a while, I realized that it couldn't be made fully backwards compatible with existing code, which limited its utility. So I gave up on that.

There was an "embedded C" group working on this issue at one point, but they don't seem to be very active any more.

One of the best ones was the DEC Extended Static Checker for Java in the late 1990s. That project died after Compaq acquired DEC and shut down research. But it formed part of Microsoft's efforts for Spec#, which has a formal verification system.

Microsoft has had a huge success with formal proof of correctness - the Static Driver Verifier. This is a system which tries to formally prove that a Windows driver can't crash the operating system. All drivers for Windows 7 have to pass this verifier to be signed, It's an impressive system which works by symbolic case analysis. It yields a proof, a counterexample, or times out analyzing too many cases. About 3% of programs time out. (If your kernel driver has undecidable behavior, it needs work.)

I headed a team that did a proof of correctness system for Pascal back in the early 1980s. That was pushing the limits of what you could do back then; verifying a small program took 45 minutes on a 1 MIPS VAX. Today, with about four orders of magnitude more CPU power, it's a practical technology.

There have been many attempts to bolt some "design by contract" features onto various languages, but they're usually not very good. The problem is saying things about collections. The hacks that try to do design by contract at run time tend to avoid expressions which examine big data structures, since they have to run them over the whole data structure every time. Real verifiers prove or disprove such things at compile time. It turns out, though, that a few standard cases for collections cover many of the usual things you want to say.

Another big issue, which Spec# handles and this Google hack apparently doesn't, is the "insideness" issue for object invariants. Object invariants are supposed to be true whenever control enters and exits an object. But what if an object calls one of its own public methods, perhaps through a long chain of calls? Now, control is inside the same object twice. That violates the invariant rule.

This class of bugs is common in window systems, where all the widget, pane, window, and event objects are frantically calling each other. It also comes up in concurrency, which I don't see Google's hack addressing either.

To see what it was like to use these fonts on the web, I created a test page. This uses dynamically downloaded fonts, which work in most current web browsers. (Firefox users need Firefox 3.6 or later.)

This sample is sized at 16 point. Smaller than that, many of the symbols are unreadable. That's something to be careful about. When you have a huge symbol set, the symbols need to be bigger. However, some of the symbols don't scale up well. If you scale up that page, the integral symbols look great, but the arrows become pixilated. Some of the symbols seem to have been were badly encoded.

This is just a raw demonstration of the font; for formulas, you'd use MathML. I'm not sure if MathML, the W3C names for math characters in HTML, and the STIX fonts are all synchronized yet. But at least you don't have to tell people "to display this page, install all these fonts first."

Speaking as a "real" computer scientist, I think you might have underestimated the time requirement. Most problems in automatic verification are either undecidable, or intractable..

As someone who's actually built an automatic verification system. no, they aren't.

It's possible to write a program with undecidable behavior. That's usually something you don't want to do, especially in real-time control code. In safety-critical real time code, you usually want brutal simplicity of design.

The practical problems with program verification are 1) C and C++ have such awful semantics, especially in the array/pointer area that they're very tough to formalize, 2) explaining to the formal system what your code is trying to do is painful and requires writing much formal notation 3) insisting that the program really match the spec implies very strict waterfall development, 4) the tools that actually work are incredibly expensive, and 5) the amount of theory that programmers must learn to do this exceeds the mathematical qualifications of most programmers.

Formal verification methods are routinely used on IC designs. The divider for the AMD K5 was one of the first applications. (Remember the Intel floating point divide bug? AMD wanted to be sure their next CPU had it right.)

No, four legs are better for a large machine. There's a tradeoff between leg working envelope, vehicle length, and top speed.

There was a big fad for six-legged insect robots in the 1990s, led by Rod Brooks at MIT. Those were very slow, very dumb, and had a very wide stance. Six legs don't scale up well. One big issue is inertia.

Double the dimensions of something, and it gets four times as strong (strength comes from cross-section) but eight times as massive (mass comes from volume.) This is called the cube-square law, and it's why there are no giant insects. For small creatures, forces like surface tension matter, but inertia doesn't. For large, fast ones, inertia dominates.

Before dynamic balance was figured out, robots tended to have very wide stances, and some had too many legs. DARPA built funded the Adaptive Suspension Vehicle at Ohio State in the 1980s. 28 feet long, six legs, seats one, no cargo capacity. Top speed 3-5 MPH on flat ground. At least three legs were on the ground at all times, and often four, five, or six. The gaits were very conservative. It was supposed to be off-road capable, but that part never worked. A sloping road was as far as they got. There was some computer control, but the thing was mostly driven by an onboard driver, using three joysticks.

With dynamic balance and traction control, the leg geometry doesn't have to be as conservative. BigDog's leg geometry is four legs with three joints each, a narrow stance, and control which allows the leg envelopes to overlap. This is close to the layout of the larger quadrupeds. (BigDog has the size and weight of a medium pony; it's bigger than dog-size.)

With four legs and a long body, pitch stability isn't too hard, but roll stability requires active control. The faster quadrupedal mammals have very narrow stances; a horse's track is less than a foot wide, narrower than its body. BigDog doesn't track quite that narrow, but it gets close. The narrow track makes tight turns possible, and allows sudden changes in yaw when needed for slip recovery or collision avoidance.

With dynamic balance and slip control, the speed can be cranked up. The six-legged machines mostly crawled; the modern four-legged machines trot, and some run. (The usual running gaits, the ones with a moment of suspension, for a quadruped are the trot, pronk, rotatory gallop, and canter. BigDog can trot and pronk; it may be able to do a rotatory gallop.) That's the real reason to go with four legs. Six legs just get in the way at speed.

BigDog's three-joint leg isn't mentioned much, but the third joint lets the control system adjust the ground contact force vector to stay within the friction cone, without changing the foot position. This is a big win when climbing hills, and the hind end needs to come under the body.

It's all about the control algorithms. Don't let the legs collide, prevent slip, recover from slip, support the body, maintain roll balance, provide propulsion, avoid obstacles, stay on course, accomplish the mission. Those are the priorities.

If you want to understand the theory behind BigDog, read Didier Papadoupolis's thesis, "Stable Running for a Quadruped Robot with Compliant Legs". The technology for BigDog came from Martin Buehler's lab at McGill University. Buehler himself quit McGill and went to work for Boston Dynamics as the chief engineer on BigDog. (Once BigDog worked, he went to iRobot.) The theory is out there in the literature. Some of it is mine.

Considering that your work looks like complete shit, you have absolutely no place to talk. Seriously, I can (and already have) create better looking models in GtkRadiant and UnrealEd.

I have a MSCS from Stanford (1985), and the field has changed since then. Back then, it was all about discrite math - number theory, combinatorics, mathematical logic, computability, and proofs. There was no number-crunching at all in the curriculum. Of course, back then, an FPU was an extra-cost option on a PC. I've actually done automated program verification work. But outside of IC design (where formal methods are routinely used), there's not much of that going on now. Now, number-crunching has come to the fore.

In the 1990s, I spent several years on what turned into ragdoll physics for games. That's all about differential equations and number-crunching. I had a hard time switching over. But I finally got used to deterministic number-crunching. I have no mathematical intuition for it, though; I took it up too late in life.

Now, the leading edge of computer science is probabilistic number-crunching. Take a look at Stanford's CS229 - Machine Learning class. That's the technology that's driving AI now, and it's working across a broad range of domains. The logicians are out, and the statisticians are in.

As a steampunk project, I've restored a Teletype Model 15, which, running uncased so you can see the insides, is an impressive piece of machinery. I have this connected to a program that polls any desired collection of RSS feeds and prints any new items that come in. Running off Reuters or the NPR news feed, it emulates a classic news ticker.

I've tried giving it a list of Twitter RSS feeds. Works fine, looks stupid. For each new twit, the motor winds up to speed, 50 pounds of machinery grinds into life, and with much clattering and banging, the machine hammers out some banal twit on a long roll of yellow paper. Twitter content is just too lame for this. Hooked to the Reuters feed, at least you get the feeling that you're keeping up with what's going on in the world. Not with Twitter.

(Incidentally, Twitter's server-side RSS implementation sucks. RSS feed servers are supposed to accept a query with a number obtained from the previous query, and if the numbers match, it means nothing changed and no new text is transmitted. Twitter implements that so badly that every poll results in transmitting the entire RSS content again, even if nothing changed. Most other RSS feeds, such as Reuters, more or less get this right.)

A dozen years ago I developed and demoed the first ragdoll physics system that worked. Among other things, I'm responsible for the "ragdoll falling downstairs" cliche; that started with a demo I did in 1997. I looked at ragdolls as a first step. I was expecting game development to go in the direction of physically-based characters driven by active control of character muscles. That hasn't happened.

The problem is partly technical and partly dramatic. The dramatic part I encountered in dealing with Hollywood types. What directors want is to specify the start and end conditions; the job of the system is to realistically get the character to the desired ending mark. In real-world stunt work, there are wires, guides, and rails that make things go the way the director wants, even when that's not physically realistic. When that's not enough, cuts are used to conceal the lack of realism.

Physics systems are inherently unidirectional - you keep working forward from the current state. This is fundamentally incompatible with directorial control. As a result, the trend in character animation has been to get enough motion capture data to cover the things you want the character to do, and use a motion splicing engine to patch the pieces together. (This, incidentally, was first used in Godzilla, the movie, for the baby 'zillas). That's become more or less the standard approach for games.

Using a character control AI to drive the character's muscles realistically has been attempted, but with modest success. Motion Factory tried this in the 1990s; their system was only kinematic, and not too successful. Havok is trying it now. For this to work, you need computerized muscle control good enough to drive a real-world robot, like Big Dog. And then it has to look good from an aesthetic perspective. It's really a hard robotics problem, which is why I was interested in it in the first place.

From a gameplay perspective, if you take the physics seriously, you lose the "superhero" capabilities of game characters. Jump off a balcony, and don't expect to land on your feet. Jumping up to a balcony? Forget it. Hand-to-hand combat works about as well as it does at the dojo. ("Your left foot was too far forward for that throw. Again!" "Yes, sensi.") Trying to control a physically realistic character via a joystick is nearly hopeless. You can't even drive a real car very well through a remote joystick, let alone a game pad. (I've actually done that; using a remote steering wheel is a huge improvement over a joystick.) In driving games for consoles, the physics is tweaked to make the car incredibly stable. (Lowering the center of gravity to below ground is a common trick.)

So what do we have? Ragdolls. "Infinitely destructible environments." Some skin deformation. Cloth. Plus rain, snow, water, and explosions that don't feed into the game play at all. (That's mostly what the "physics cards" do.)

I have a Model 15 Teletype, a 1930 design built in 1944, not only working, but printing RSS news feeds. The Reuters RSS feed gives me a nice news report. Each time Reuters posts a new story, the Teletype motor turns on, the big machine prints the story, and it shuts down again.

I also set it up so that I can send text messages from the Teletype keyboard. All upper case, of course.

These machines are incredibly overdesigned, which is why they still work after 65 years. Unless they've been physically damaged, it's not that hard to get one running again. Mine just required thorough cleaning and oiling (over 500 oiling points), a new ribbon, and a roll of paper. I had to build a level-converting interface for the thing; it needs a 60mA current loop with 120VDC powering it. So I designed a small PC board for that.

A standard PC serial port will talk to it, at 45.45 baud, 5 bits, 1.5 stop bits, no parity. Which Windows will happily do. (Linux won't; the Linux scheme for selecting baud rates uses a fixed list of baud rates left over from the PDP-11 era. There are driver-level hacks to get around this, but the stock serial driver won't do it.) I wrote a Python program to handle the Teletype's Baudot issues and machine control, and to poll RSS feeds, printing each new story exactly once. It also does NOAA weather reports.

I've tried various RSS feeds. Reuters has the cleanest ones for this purpose. Each story comes with a heading and a brief, coherent summary. Most of the other RSS news feeds either just have the headlines, or truncate each story arbitrarily, ending it with "...". Reuters adds about one new story per hour, on average. It just printed "OBAMA TO NAME WHITE HOUSE CYBERSECURITY CZAR". (This is an upper-case-only machine, remember.)

Once I build a transparent case for the machine, I'm going to loan it to the Exploratorium or the Computer Museum. It will be set up to print news, and maybe incoming text messages so kids can text to it.

Suggest some good RSS feeds for demo purposes. Reuters has about one story per hour. A feed that produces something every 5-10 minutes would be useful.

It's time for software to grow up.

I proposed this in 2000 as a penalty for Microsoft in their antitrust trial. That would have been a big step forward.

The claim that "the vendor doesn't know the environment in which the software will be used" is bogus. Car companies have no idea where you will drive your car, or on what kind of roads. They have a far worse problem than any software maker. Yet they have to accept serious liability obligations.

Provided that this is implemented as a constraint on commerce, it's not an issue for free software when distributed for free. However, companies that package up free software and resell it (Red Hat, Novell, etc.) will face liability. That's as it should be.

No offense to DARPA, not all of the navigation and vision algorithms in those cars with a whole set of high speed computers are really practical for use on smaller home service robots.

Vision works better on home service robots that it does outdoors. Outdoors, getting a long enough baseline for a stereo pair is hard, except through motion vision. Humans only have stereo out to a few meters, anyway. SLAM (Simultaneous Location and Mapping) for mobile robots is getting quite good. Willow Robotics demoed their system at RoboDevelopment a few months ago, and the latest issue of IEEE Trans. on Robotics, a special issue on SLAM, indicates how good that's become.

But machine learning is facing some strong limitations when compared with the abilities of biological systems in coping with unsupervised learning in uncertain and dynamic environments.

I recently went over to Stanford to see the CS229 project presentations, and it's very impressive what small teams of students are getting done in one quarter. Self-guiding robot helicopters, for example. The field has moved away from neural nets; Bayesian statistics, with real theory underneath, works better.

the balance and slip control of Big Dog, applies to quadrupeds with the similar mechanical characteristics. If you are trying to imply that the results are relevant to humanoids, I suggest you read up on the loads of material on everything from 3d linear inverted pendulum model to spin angular momentum regulation and control for humanoids.

Been there, done that, own the patent on legged slip control. For systems which really use dynamic balance, the number of legs doesn't matter all that much from an algorithm standpoint. In fact, most real progress has been made by first getting the one-legged case to work. Key insights: 1) balance has priority over movement, 2) slip/traction control has priority over balance, 3) legs need three joints, not two, so you can play with the force vector at ground contact independent of foot position, and 4) legs are viewed as assets to be deployed to manage traction, balance, and propulsion. "Gaits" are an emergent behavior, the state into which things settle down when movement is not disrupted.

Indeed.

The reason software is so bad is that the customers absorb the cost of defects. That's a political decision. Cars used to be that way; today, if a car even stalls unexpectedly, that's considered a manufacturing defect. In the US, the manufacturer has to pay for the recall to fix the problem. Cars are far more reliable, and much safer, as a result.

In a few industries, the software developer is financially liable for errors. The gambling industry works that way. The companies that run lotteries pay back a few percent of their revenue as penalties for failures and errors. (And they try very hard not to have expensive errors.)

Back before the Bush administration caved on the Microsoft antitrust case, I proposed the Full Warranty remedy. The FTC took a look at this issue in 2000, but the Bush Administration didn't do anything. It may be time to revisit this.

It's amusing seeing Strostrup whining that schools are teaching Java instead of his C++. The problem with C++ is Strostrup. He's in denial about many of the fundamental problems of C++. He's publicly stated that there's nothing major wrong with C++. If that was the case, we wouldn't need Java and C#, which are, after all, attempts to improve on C++.

Down at the bottom, the fundamental problem with C and C++ is the "pointer=array" concept. That was OK for 1978, but it didn't scale well. It's the cause of most of the buffer overflows in the world. C and C++ don't even have syntax for properly talking about the size of an array parameter. That's just broken. C and C++ need something like conformant array syntax for parameters and in other contexts where one needs to talk about the size of an array.

The second fundamental problem with C and C++ is that the programmer must obsess on "who owns what", and the language not only doesn't provide help with this, it doesn't even have syntax for talking about it. There's no distinction between a pointer that "owns" an object and one that just "uses" it. Yet if the programmer doesn't carefully make that distinction, the program will have either memory leaks or dangling pointers.

The trend in C++, since templates went in, is to try to wallpaper over the problems with the underlying model. It never quite works; the mold always seeps through the wallpaper. Container classes almost, but not quite, succeed at encapsulation. There's almost always some place where a raw pointer has to be allowed to leak out. The standards committee has gone off on a "generic programming" tangent, with emphasis on weird template features used by few and used correctly by fewer. Just because you can abuse the C++ template system as a term-rewriting engine doesn't mean you should do that in production code. This results in a whole new class of incredibly obscure compile-time bugs. The standards committee has been thrashing for over a decade in this area; in the 1990s, the new version was to be "C++9x"; now it's "C++0x", and since we're close to 2009 already, "C++1x" looks like the reality.

C++ is the only major language to have hiding ("abstraction") without memory safety. No previous language had it, and no later language repeats that mistake.

Back around 2001, I made an effort to do something about it, but the political hassle was more than I had time for.

I've done work like that. But it was a long time ago, back in the early 1980s. It took over an hour on a VAX 11/780 to verify a few hundred lines of code. (See the example auto engine control program that starts on page 55; this was funded by the Ford Motor Company.) Today, it would take under a second.

Proof of correctness systems are quite feasible, but a pain to use. They also tend to be developed by people who are in love with the formalism, which can be a problem for programmers. Formal specifications are hard to write and harder to verify, which is the real problem. However, automatically grinding through code and finding all potential overflow and subscript errors is quite practical. We were doing that in 1984. You get about 95% of the checks verified automatically, and then have to provide additional information to get the rest of them satisfied. That's where the human effort goes. If you can formalize the concept of "bad stuff that should never happen", which is something NSA tries hard to do with "mandatory security policies", you have a hope of verifying it.

There have been some impressive proof efforts over the years. There's been quite a bit of effort devoted to proof of correctness for hardware at the VHDL level. Boyer and Moore did a proof of correctness for AMD's FPU after Intel had the famous Pentium divide bug.

What really set back the field was the replacement of Pascal by C. Pascal has well-defined semantics that can be formalized. C, and C++, do not. That's why I got out of the field.

There was some nice work on Modula verification at DEC in the 1990s, but it died with DEC. Some of the same people went to Microsoft and built a verifier for a dialect of C#. There's been some work at Rational over the years. But it's never gone mainstream.

The prohibition on "multiple exits" or returns comes from a misunderstanding of early program proving technology. As one of the few people who ever built a real proof of correctness system, I know that's just not a problem.

There are some topological restrictions on program proving, but you can't violate them with "break" or "return". You need "goto" to really screw up. The actual topological constraint is that backwards control paths must not cross.

The basic requirement for proving loops is that there must be some section in the loop through which control must pass on every iteration. Somewhere in that section must go the loop invariant and the termination measure.

Nobody does this for software any more, although, interestingly, full-scale machine proof of correctness of hardware logic in VHDL is not that unusual. There are commercial tools for that.

The real problem with program verification is the C programming language. In C, the compiler has no clue what's going on with arrays, because of the "pointer=array" mistake. You can't even talk about the size of a non-fixed array in the language.

This is the cause of most of the buffer overflows in the world. Every day, millions of computers crash and millions are penetrated by hostile code from this single bad design decision.

That's why I got out of program verification when C replaced Pascal. I used to do this stuff.

Good program verification systems have been written for Modula 3, Java, C#, and Verilog. For C, though, there just isn't enough information in the source to do it right. Commercial tools exist, but they all have holes in them.

Several posters have cited the "halting problem" as an issue. It's not.

First, the halting problem does not apply to deterministic systems with finite memory. In a deterministic system with finite memory, eventually you must repeat a state, or halt. So that disposes of the theoretical objection.

In practice, deciding halting isn't that hard. The general idea is that you have to find some "measure" of each loop which is an integer, gets smaller with each loop iteration, and never goes negative. If you can come up with a measure expression for which all those properties are true, you have proved termination. If you can't, the program is probably broken anyway. Yes, it's possible to write loops for which proof of termination is very hard. Few such programs are useful. I've actually encountered only one in a long career, the termination condition for the GJK algorithm for collision detection of convex polyhedra. That took months of work and consulting with a professor at Oxford.

The real problem with program verification is the C programming language. In C, the compiler has no clue what's going on with arrays, because of the "pointer=array" mistake. You can't even talk about the size of a non-fixed array in the language. This is the cause of most of the buffer overflows in the world. Every day, millions of computers crash and millions are penetrated by hostile code from this single bad design decision.

That's why I got out of program verification when C replaced Pascal. I used to do this stuff.

Good program verification systems have been written for Modula 3, Java, C#, and Verilog. For C, though, there just isn't enough information in the source to do it right. Commercial tools exist, but they all have holes in them.

There's nothing good to program in. This is a serious problem.

We have C. C isn't a bad language, but the "pointer=array" concept, while it provided some performance gains in the PDP-11 days, continues to cause millions of crashes and intrusions every day. The fundamental problem is that you can't even express the size of an array in the language. Given that, the odds of consistently getting subscripts right is low. This could be fixed, but it will never happen.

There's C++. C++ has lost its way, as I've pointed out before. The C++ committee is off in template la-la land, putting in features that few will use and fewer still will use correctly. (Coming soon: "concepts"). The real problem with C++ is that it's no safer than C, but hides more.

There were once better languages. Delphi is better, but it's Borland. Modula 3 was a good systems programming language, but it died with DEC. Various attempts at improvement, from Ada to Eiffel to Sather, have almost died off. Amazingly, "D", which is Walter Bright's successor to C++, has a measurable market share.

Some progress is being made on numeric issues, like compiling Matlab to efficient code for parallel hardwware. But that doesn't help systems programming much. Hard-compiled Python would have potential, if Guido wasn't against it. (Python has a speed penalty of about 10x to 60x over C/C++. Maybe at some point Google management will decide that a hard-compiled Python system would be cheaper than building additional data centers at former aluminum-smelter sites.)

As for garbage collection, it's a headache. "Finalizer" and "destructor" semantics get weird. (See "Managed C++") Reference counting leads to saner semantics and repeatable timing, but is inefficient unless the compiler knows how to hoist reference count updates out of loops. (Incidentally, about 90% of subscript checks can be hoisted out of loops, and you can almost always hoist them out of inner FOR loops. So subscript checking is almost free if done right.) Note that Perl is reference-counted, and Perl programmers don't spend much attention on memory management. If you have strong and weak pointers, reference counting, and treat cycles as errors, you don't really need garbage collection.

Says the guy who patents PD controllers for animating human figures.

http://www.animats.com/
Our technology for high-quality ragdolls is patented. This broad patent covers most spring/damper character simulation systems. If it falls, it has joints, it looks right, and it works right, it's probably covered by our patent.

I used to do animation tools for physically based animation, and got some idea of the Hollywood view of dynamics.

A basic concept in filmmaking is that the endpoint of a motion is predetermined. Directors think in terms of "here, then here, then there". The path desired is quite likely to be physically unrealistic, and may have to be pieced together from several shots.

A real physics simulator just isn't "directable" enough. What's used in practice is a combination of hand animation, piecing together motion capture, a collection of clever tricks to make real-world objects go where you want them, and lots of cuts to hide discontinuities. The MTV-style "one cut per second" approach to action scenes makes it even easier.

Much the same thing happens in games, except that you have to allow a user with limited control to drive a character with too many degrees of freedom and not enough embedded smarts to manage movement against real-world physics. This is why, in most sports games, you see beautiful motion-captured motion interspersed with strange jerks as motions are blended in ways that are continuous but nonphysical.

In most driving games, the physics is totally unrealistic. The wheel adhesion is huge, the CG is very low (often below the ground) and it's very common to lock roll rate once the vehicle is tilted beyond recovery angle, so that the vehicle rolls all the way over and lands upright. Driving a full sized car through a remote joystick works badly (we tried this with our DARPA Grand Challenge vehicle once, then immediately bought a MoMo steering wheel and interfaced it) and game controller joysticks are even worse. So the vehicle model has to be incredibly forgiving.

There is a classic of computational Hollywood physics worth noting. In the Bond movie, "The Man with the Golden Gun" (1974), a car is driven over a ruined arch bridge at high speed, executes a 360 degree roll, and lands on the far side. It really did do that. The dynamics were calculated by the Cornell Aeronautical Laboratory (now CALSPAN) and the ramp was constructed to make it happen consistently if the vehicle was driven at the correct speed. But there's a cheat there, too. The car had a fifth, solid wheel underneath which hit a rail on the launch ramp to initiate the roll. It wasn't possible to induce enough roll rate fast enough through the vehicle suspension.

Here's some code of mine.

• mutexlock.h - queuing and locking primitives in C++ for QNX. Little primitives that have to be right, and are hard to code correctly. These ran on our DARPA Grand Challenge vehicle.
• algebra3.h - basic functions for 2D, 3D, and 4D matrices and vectors, all in C++ and all inline. The basic code is from Graphics Gems, but it's been rewritten to be 100% inline. Useful for game and graphics work. Used as part of Falling Bodies.
• obvious.c - the original obvious password detector, from 1984. Use this to decide if a password is "strong enough". Rejects all English words, yet doesn't require access to a dictionary file. Note this is in K&R C; it predates ANSI C.

Here's some code of mine.

• mutexlock.h - queuing and locking primitives in C++ for QNX. Little primitives that have to be right, and are hard to code correctly. These ran on our DARPA Grand Challenge vehicle.
• algebra3.h - basic functions for 2D, 3D, and 4D matrices and vectors, all in C++ and all inline. The basic code is from Graphics Gems, but it's been rewritten to be 100% inline. Useful for game and graphics work. Used as part of Falling Bodies.
• obvious.c - the original obvious password detector, from 1984. Use this to decide if a password is "strong enough". Rejects all English words, yet doesn't require access to a dictionary file. Note this is in K&R C; it predates ANSI C.

They really have got a broad patent.
The first one has a mistake:

Anti-slip control for a legged robot and realisitc simulation of a legged creature

does this make it invalid?

from here: http://animats.com/topics/patents.html

I just hope this guy does not kill off NaturalMotion with his overly broad patents.

Fixing the "safety problem," as you call it, would involve an increase in execution time.

That's a common belief, because the safe languages we have now are mostly inefficient ones, but it's wrong. Subscript checking is cheap if done right, in the compiler with appropriate optimization, because most subscript checks can be hoisted out of inner loops. This was done in a British Pascal compiler in the 1980s, but I don't have the reference handly.

The problem in C and C++ is that there are too many cases where the compiler doesn't even know how big an array is, so the compiler can't check. If you try to do subscript checking in collection classes, the checking is inefficient because the compiler doesn't know enough to optimize it.

Here's the general idea of how to do it right:

float sumarray(size_t n, float tab[n]) /* C99-type array size notation */
{ float sum = 0.0;
for (size_t i=0; i<n; i++)
{ sum += tab[i]; }
return(sum);
}

That code implies a test for i < n at tab[i]. That would seem to add overhead. But if we allow the compiler to hoist checks upwards, that test floats to the top of the FOR statement. We then have the test of the FOR statement, i < n. So we have "i < n implies i < n, as the test, which symbolically evaluates to TRUE at compile time and can be eliminated. The compiler can thus this do this subscript check with zero overhead.

That's how you get safety without overhead.

Certainly there are situations where the checks can't be performed entirely at compile time, but usually, they can be pulled out of an inner loop by standard compiler hoisting and strength reduction techniques. So the overhead is quite low in code hot spots, where it matters.

Note the syntax float sumarray(size_t n, float tab[n]). That's C99 variable array syntax. Instead of writing float tab[], or worse, float* tab, you actually give the array length. This doesn't cost anything, because the length isn't actually being passed. It just tells the compiler where the length information is to be found, should it be needed.

At a call to sumarray, checking is also possible. Consider

float tab nums[1000];
...
float tot = sumarray(tab, 1000);

I've suggested that C99 array syntax be generalized to give parameters the scope of the entire declaration, allowing float sumarray(float tab[n], size_t n), where n is referenced before its declaration. This allows standard C idioms like int write(int fd, char buf[n], size_t n).

Microsoft R&D is working in this direction for C#. Check out the "Spec#" effort. The trouble with C++ is that the language is so broken that you can't use such technologies.

We had much of this technology working in the early 1980s, but machines were too slow back then to tolerate the compile times. With the 3000x improvement in CPU speed since then, that's no longer a problem.

The main reason program verification didn't catch on was that it was hopeless for C and C++. The semantics of those languages were so messy that formalizing them was nearly hopeless.

Java and C#, however, are good enough. (So were Pascal, Modula, and Ada.)

Here's the manual for the Pascal-F verifier, a system written by a team I headed back in the early 1980s. This was a proprietary system done internally for Ford Motor Company. Take a look at the example real time engine control program beginning on page 155. It was painfully slow back then; it took 45 minutes of VAX 11/780 time (1 MIPS) to verify that program from a cold start. Today, it would take about a second.

What's being proved in that example? First, that there are no subscripts out of range or arithmetic overflows. Second, that all loops terminate. (Yes, you can prove that for most useful programs; the halting problem applies only to pathological programs.) Third, that the following constraints hold:

• fuelpumpon implies (tickssincespark < (1000*ms)); if fuel pump is on, spark must occur within 1 sec.
• (enginespeed < rpm(1)) implies (not fuelpumpon); fuel pump must be disabled if the engine is not rotating
• cylssincespark <= 1; a spark must be issued for each cylinder pulse

Useful stuff, the conditions needed to keep the engine running.

This is "design by contract" with teeth. Each function is checked to insure that it always satisfies its exit conditions if its entry conditions are satisfied by the caller, and that the function doesn't overflow, subscript out of range, or fail to terminate. Each call is checked to insure that its entry conditions are always satisfied. The end result is a guarantee that those properties hold for the whole program.

This is a very valuable check. It insures that caller and callee are in agreement on how to call each function. That's the cause of a huge number of software bugs - the caller made some incorrect assumption about the function being called, or the function didn't check for something which it needed to check. Both of those can be statically machine checked.

It's not easy to get a program through formal verification with a verifier like that one. The verifier does almost all the work on easy sections of code, but where correctness depends on anything non-trivial, you have to work with the theorem prover to get the proofs through. This isn't easy. The DEC Java checker and Microsoft's Spec# checker aren't as hard-line.

Twenty-two years on, here's my obvous password detector. This is C source code I wrote in 1984. This simple piece of code will prevent the use of passwords that are English words, by requiring that the password have at least two sequences of three letters not found in the dictionary. The "dictionary" is compressed down to a big table of hex constants; it's a 27x27x27 array of bool, with a 1 for each triplet found in the UNIX dictionary. So the code is simple, self-contained, and does no I/O.

Put this in your password-change program and dictionary attacks stop working.

The code is a bit dated; this is original K&R C, not ANSI C.

I should do a Javascript version and give that out. The code is so small that it could easily be executed on user-side password pages.

What you're looking at is a one-legged hopper. Locomotion researchers find it useful to work on one-legged hoppers because the system is simple enough to be analyzed analytically.

The new feature of this leg seems to be that it has three active joints with sufficient power behind them for jumping. Most legged robots, such as the BDI Big Dog, only have two active joints in the leg, although some have a weak or passive ankle. This is enough to position the leg to any point in the working envelope, and it's not obvious what a third joint buys you. ASIMO has an "ankle", but it's used only to align the foot with the ground, not for active running; ASIMO runs flat-footed, not on the ball of the foot. This Toyota machine seems to have both an ankle and a toe joint.

This is a big win, as I described back in 1995 in my "Why Legs have Three Joints" paper. With three joints involved in running and jumping, you gain control over the force vector for ground contact, which allows slip control. Also, the hip joint (which is usually the most powerful) can be used more effectively; the lower joints position the leg so that the hip muscles can do most of the work. For humans, this is subtle, because the ankle-toe distance is small. It's much clearer for horses, where the hind leg has three sections of roughly equal length.

Im not going to http://www.animats.com/ to get more totally useless (crappy plugin thingy) free spamware..

It is not possible for a program to analyze another program and find all the bugs; see halting problem .

Wrong. It is quite possible to analyze a program and find all the bugs that violate the language constraints (null pointers, buffer overflows, etc.). That's what program verification is for. For some programs, you can't tell whether a bug condition will occur, so you treat that as a bug.

Automated program verification is a good idea that went away because C and C++ have such ambiguous semantics. It's hopeless for those languages. The "pointer equals array" concept alone makes it very tough, because the language has no idea how big an array is. Worst idea in the language, and the root cause of buffer overflows.

Good verifiers were written for Pascal (I headed one of those projects), a good one was written for Java (at DEC, just before DEC went under), and Microsoft is working on one for C#.

I built something like that while in high school, which really dates me.

Been there, done that. At the 1997 Softimage user conference, we showed our physics engine, Falling Bodies. This was the first ragdoll physics system that actually worked right. We had a 3D model of a big mecha about 20m high, which you could keyframe and then let the physics engine take over. Someone playing with it keyframed it on the ground on one frame, and about 20 meters higher in the next frame. Then they started the physics engine. This launched the huge character straight up at about mach 2, and it rapidly shrank into a dot. But the frame counter kept running, and after about twenty seconds, the dot started to get bigger again. The huge character hit the ground, bounced, rolled, slid, and eventually came to rest.

It really does look better if you handle the hard cases correctly.

If motion in free flight looks wrong, that's probably intentional.

But if big objects bounce as if they're very light, that's a fundamental limitation of impulse-constraint physics engines. All bounces occur instantaneously in such systems. (That's what an "impulse" means; an infinite force applied for zero time with finite energy, leading to an instantaneous change in velocity.) So big objects don't appear to have "weight". We call this the "boink" problem.

We solved that problem in 1996-1997, but it takes more compute power to do it right, so most physics engines take the cheap approach. This is the main reason physics in games consistently looks unrealistic.

When our ragdolls fall down, it looks like they're hurting. (Then again, do you want that level of realism in death scenes?)

Our approach produces better-looking movement than the low-end physics packages. We don't have the "boink problem", where everything bounces as if it were very light. Heavy objects look heavy. Our physics has "ease in" and "ease out" in collisions, as animators put it, derived directly from the real physics. When we first did this, back in the 200MHz era, it was slow for real time (a two-player fighter was barely possible) but now, game physics can get better.

Take a look at our videos. Few if any other physics systems can even do the spinning top correctly, let alone the hard cases shown.