proj-oot-ootSafetyNotes1

"Swift eliminates entire classes of unsafe code. Variables are always initialized before use, arrays and integers are checked for overflow, and memory is managed automatically."

--

apparently, one good effect of the requirement that every variable be used in Golang is that it forces programs to check return values

--

[–]jfagercontributor 16 points 22 hours ago

Looks like the safety features are: static types, forced initialization, Option, arc, no automatic coercions, bounds checking.

I don't see anything in the book about concurrency.

    permalink

[–]scribble_child 12 points 17 hours ago

For the lazy, arc ≡ automatic reference counting.

    permalink
    parent

--

http://spinroot.com/gerard/pdf/P10.pdf is a great read. it has 10 simple rules for safety.

" 1. Rule: Restrict all code to very simple control flow constructs – do not use goto statements, setjmp or longjmp constructs, and direct or indirect recursion.

Rationale: Simpler control flow translates into stronger capabilities for verification and often results in improved code clarity. The banishment of recursion is perhaps the biggest surprise here. Without recursion, though, we are guaranteed to have an acyclic function call graph, which can be exploited by code analyzers, and can directly help to prove that all executions that should be bounded are in fact bounded. (Note that this rule does not require that all functions have a single point of return – although this often also simplifies control flow. There are enough cases, though, where an early error return is the simpler solution.)

2. Rule: All loops must have a fixed upper-bound. It must be trivially possible for a checking tool to prove statically that a preset upper-bound on the number of iterations of a loop cannot be exceeded...This rule does not, of course, apply to iterations that are meant to be non-terminating (e.g., in a process scheduler). In those special cases, the reverse rule is applied: it should be statically provable that the iteration cannot terminate.

...

3. Rule: Do not use dynamic memory allocation after initialization.

...

4. Rule: No function should be longer than what can be printed on a single sheet of paper in a standard reference format with one line per statement and one line per declaration. Typically, this means no more than about 60 lines of code per function.

5. Rule: The assertion density of the code should average to a minimum of two assertions per function. Assertions are used to check for anomalous conditions that should never happen in real-life executions. Assertions must always be side-effect free and should be defined as Boolean tests. When an assertion fails, an explicit recovery action must be taken, e.g., by returning an error condition to the caller of the function that executes the failing assertion.

...

A typical use of an assertion would be as follows:

if (!c_assert(p >= 0) == true) { return ERROR; }

with the assertion defined as follows:

  1. define c_assert(e) ((e) ? (true) : \ tst_debugging(”%s,%d: assertion ’%s’ failed\n”, \ __FILE__, __LINE__, #e), false)

In this definition, __FILE__ and __LINE__ are predefined by the macro preprocessor to produce the filename and line-number of the failing assertion. The syntax #e turns the assertion condition e into a string that is printed as part of the error message.

...

6. Rule: Data objects must be declared at the smallest possible level of scope.

Rationale: This rule supports a basic principle of data-hiding. Clearly if an object is not in scope, its value cannot be referenced or corrupted. Similarly, if an erroneous value of an object has to be diagnosed, the fewer the number of statements where the value could have been assigned; the easier it is to diagnose the problem....

7. Rule : The return value of non-void functions must be checked by each calling function, and the validity of parameters must be checked inside each function.

... In its strictest form, this rule means that even the return value of printf statements and file close statements must be checked. One can make a case, though, that if the response to an error would rightfully be no different than the response to success, there is little point in explicitly checking a return value.... In cases like these, it can be acceptable to explicitly cast the function return value to (void) – thereby indicating that the programmer explicitly and not accidentally decides to ignore a return value.

8. Rule: The use of the preprocessor must be limited to the inclusion of header files and simple macro definitions. Token pasting, variable argument lists (ellipses), and recursive macro calls are not allowed. All macros must expand into complete syntactic units. The use of conditional compilation directives is often also dubious, but cannot always be avoided. This means that there should rarely be justification for more than one or two conditional compilation directives even in large software development efforts, beyond the standard boilerplate that avoids multiple inclusion of the same header file. Each such use should be flagged by a tool-based checker and justified in the code.

Rationale: The C preprocessor is a powerful obfuscation tool that can destroy code clarity and befuddle many text based checkers....Note that with just ten conditional compilation directives, there could be up to 2^10 possible versions of the code, each of which would have to be tested– causing a huge increase in the required test effort.

9. Rule: The use of pointers should be restricted. Specifically, no more than one level of dereferencing is allowed. Pointer dereference operations may not be hidden in macro definitions or inside typedef declarations. Function pointers are not permitted.

Rationale: Pointers are easily misused, even by experienced programmers. They can make it hard to follow or analyze the flow of data in a program, especially by tool- based static analyzers. Function pointers, similarly, can seriously restrict the types of checks that can be performed by static analyzers and should only be used if there is a strong justification for their use, and ideally alternate means are provided to assist tool-based checkers determine flow of control and function call hierarchies. For instance, if function pointers are used, it can become impossible for a tool to prove absence of recursion, so alternate guarantees would have to be provided to make up for this loss in analytical capabilities.

10. Rule: All code must be compiled, from the first day of development, with all compiler warnings enabled at the compiler’s most pedantic setting. All code must compile with these setting without any warnings. All code must be checked daily with at least one, but preferably more than one, state-of-the-art static source code analyzer and should pass the analyses with zero warnings.

...

"

---

Animats 19 hours ago

"We get the software we deserve."

Painfully true. There are techniques for writing better software. They work. They take longer and cost more. They are not widely used outside aerospace.

reply

dgemm 19 hours ago

Is there a high level overview somewhere I can read? Don't even know what to google here.

reply

throwawayf2o 18 hours ago

http://spinroot.com/gerard/pdf/P10.pdf (some are more/less appropriate for non-embedded-systems)

In general, the answer typically involves formal specification and formal methods that check the code against these specifications, combined with testing and coding standards that result in analysable code.

More references:

https://www.cs.umd.edu/~mvz/cmsc630/clarke96formal.pdf

http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

reply

pjmlp 12 hours ago

Search for high integrity software.

For example, with MISRA it may be C, but feels like Ada.

http://www.misra.org.uk/

Or Spark similarly for Ada

http://www.spark-2014.org/

reply

tormeh 18 hours ago

You might want to look into coding standards for C and special languages like Ada (like C, but less writeable, more readable with strong types) and Esterel (deterministic multithread scheduling). Seriously, Esterel is probably the coolest thing you'll read about this week.

There's also various specification languages for multithreaded behaviour, which allows you to analyse your programs behaviour using software tools, for example SPIN[0].

0: http://en.wikipedia.org/wiki/SPIN_model_checker

reply

roma1n 3 hours ago

Yup. How a DO-178-like integrity level is not mandatory for medical devices is troubling.

reply

---

 acomjean 7 hours ago

I wrote software for Radars. Kind of important (not like plane software). We used Ada alot, which in my estimation helped. Software was reviewed. Tests were reviewed. Reliability was favored over other things (for example recursion was discouraged). We used Ada's constrained types (this value is between 1 and 99, if it goes out of range, throw an exception).

For external hardware inputs, we had software simulating the messages when we couldn't get the real equipment in the lab. We were writing software for a radar that didn't yet exist.

And it was tested and tested and tested and tested.....

The when the pieces came together in integration. They tested and tested. An when they built the physical radar, the software worked. A few configuration things here and there needed adjusting.

Actually testing was built into the software. When it came up it would talk to the physical parts to make sure everything was communicating ok before it could start running.

Was it bug free? Probably not. You can't test every possible scenario. But we took the work seriously. It took longer to get code done than any other environment I've been in, but the code ended up very solid quality.

reply

outworlder 6 hours ago

> Actually testing was built into the software. When it came up it would talk to the physical parts to make sure everything was communicating ok before it could start running.

I've been wondering about this for a while. We tend to run unit tests, integration tests, whatever tests, while the software is in development. However, once it is in "production" (for whatever definition of production), usually no tests are performed. At most, there's some sort of metrics and server monitoring, but nothing in the actual software.

It's a work of fiction, but Star Trek has these "diagnostics" that are run, with several levels of correctness checks, for pretty much everything. In your typical app, it could be useful to ask it to "run diagnostics", to see if everything was still performing as expected.

reply

dugmartin 5 hours ago

Early in my career I worked on military flight data recorders, including the development of the software for the F-22's "black box". Those systems have SBIT, IBIT, PBIT and MBIT sub-systems were BIT is "built in test" and S = startup, I = initiated, P = periodic and M = maintenance. I remember making the Star Trek diagnostic joke myself when I was assigned the SBIT work.

Each BIT does varying level of testing based on it's runtime budget but there are a lot of very basic tests that don't make much sense until you see your first field report of some register bit "sticking". Its much better to ground a plane that can't add 1+1 than to find that out in mid-flight.

reply

Serow225 3 hours ago

Yup, as far as I remember all the avionics hardware I saw had these types of BITs built in.

reply

neurotech1 2 hours ago

An F-22 had a FCS failure and didn't realize takeoff. The pilot didn't do a IBIT on the FCS as required, therefore wasn't aware that all 3 rate sensors latched up. The jet was uncontrollable once it left the ground, and the pilot ejected safely. [0]

As I recall, they modified the sensors to avoid latch up (extra pullup resister) and updated the FCS software to provide a warning if all 3 sensors return zero output. Even though this wasn't really an error in the FCS software, It could be argued that it failed to detect an erroneous input from 3 redundant sensors that latched up for the same reason.

This is a classic example of a pilot who misunderstood the pre-takeoff checklist procedure and cost the USAF a $325m aircraft.

[0] http://usaf.aib.law.af.mil/ExecSum2005/F-22A_20Dec04.pdf

reply

npatrick04 1 hour ago

There's actually a decent probability of memory corruption in space applications due to radiation. So in addition to checking communication across busses, application checksums are typically run continuously.

reply

rzzzt 6 hours ago

Dropwizard (a web application framework/library) incorporates the idea of such health checks, and you can also implement additional ones specific to the application. It is encouraged to run them periodically in production to ensure that the database connection is still up, threads are not stepping on each others' toes, etc.

https://dropwizard.github.io/dropwizard/manual/core.html#hea...

reply

joshrotenberg 6 hours ago

That uses the metrics library by the same author. Very handy stuff in there for development and production.

https://dropwizard.github.io/metrics/3.1.0/

reply

jerf 6 hours ago

It doesn't necessarily take much work to run integration tests as diagnostics on production, especially if you plan on it in advance. I've had good success with it.

Of course there's a certain level of destructive testing you can't do live, but that you really ought to do on your development system, load testing being a simple example. It behooves the wise developer to keep these quite separated in the code. :)

reply

Tloewald 6 hours ago

The project I'm working on (for the Federal government no less, and very much not life and death) involves having test data in the production system and tests that run in the production system. (I was impressed by this when I found out.)

reply

clearf 1 hour ago

Make sure they're well separated! c.f. http://www.wsj.com/articles/SB100014240527487033765045754919...

reply

omouse 6 hours ago

That would be called reliability testing and it's why Netflix has chaos monkey to throw a wrench into things.

reply

lostcolony 4 hours ago

Also conformity monkey.

reply

z3t4 6 hours ago

A lot of ppl get this backwards, that a stable program should never "crash". While it's actually the opposite, it should throw errors at every opportunity to do so.

The errors should then be logged and the program should be restarted by a watcher process.

Here's an example on how you can both log errors and e-mail them if a process crash, using a startup script (Linux, Ubuntu):

  exec sudo -u user /bin_location /program_path 2>&1 >>/log_path | tee -a /error_log_path | mail mail@domain.com -s email_subject

reply

peteretep 20 minutes ago

If an error is caught and handled, calling it a crash seems disingenuous.

reply

tormeh 6 hours ago

A watchdog pattern just splits the program into several processes, the program as a whole still never crashes.

reply

yellowapple 5 hours ago

This is how Erlang (for example) gets its reputation of being "nine-nines" capable (i.e. capable of 99.9999999% uptime, or downtime on the order of milliseconds per year). Erlang (and Elixir and LFE) software following the OTP framework is usually ordered into "supervision trees" - layer upon layer of Erlang processes managing other Erlang processes in turn managing other Erlang processes, all potentially distributed across multiple Erlang VM (nowadays BEAM) instances.

reply

mturmon 4 hours ago

Further to your point, here's the guideline, and rationale, from Gerard Holzmann's document on recommended coding practices for C at NASA/JPL:

1. Rule: Restrict all code to very simple control flow constructs – do not use goto statements, setjmp or longjmp constructs, and direct or indirect recursion.

Rationale: Simpler control flow translates into stronger capabilities for verification and often results in improved code clarity. The banishment of recursion is perhaps the biggest surprise here. Without recursion, though, we are guaranteed to have an acyclic function call graph, which can be exploited by code analyzers, and can directly help to prove that all executions that should be bounded are in fact bounded. (Note that this rule does not require that all functions have a single point of return – although this often also simplifies control flow. There are enough cases, though, where an early error return is the simpler solution.)

This is rule 1 of 10, so he apparently feels strongly about "banishing recursion." Gerard was formerly at Bell Labs and is also a fellow of the ACM and a member of the NAE.

reply

robotresearcher 3 hours ago

tldr version: Because you want (i) an acyclic function call tree of (ii) predictable depth.

reply

eropple 1 hour ago

That reminds me--a friend was telling me earlier today about a piece of software he was working on that only allowed forward jumps. (It ensures that the program halts.)

reply

TheLoneWolfling? 36 minutes ago

It does slightly more than that - it provides a cheap computation of the upper bound of how long it will take.

reply

eropple 30 minutes ago

Yeah, that too. Come to think of it, that was probably more his concern than just halting.

reply

shanemhansen 6 hours ago

I've seen some software that does lots of tests on startup. One software I used (ATG) validated all the ORM mappings against the currently configured database on startup by default.

reply


" Protection against stack-based memory corruption errors using SafeStack?

This patch adds the safe stack instrumentation pass to LLVM, which separates the program stack into a safe stack, which stores return addresses, register spills, and local variables that are statically verified to be accessed in a safe way, and the unsafe stack, which stores everything else. Such separation makes it much harder for an attacker to corrupt objects on the safe stack, including function pointers stored in spilled registers and return addresses. You can find more information about the safe stack, as well as other parts of or control-flow hijack protection technique in our OSDI paper on code-pointer integrity (http://dslab.epfl.ch/pubs/cpi.pdf) and our project website (http://levee.epfl.ch).

The overhead of our implementation of the safe stack is very close to zero (0.01% on the Phoronix benchmarks). This is lower than the overhead of stack cookies, which are supported by LLVM and are commonly used today, yet the security guarantees of the safe stack are strictly stronger than stack cookies. In some cases, the safe stack improves performance due to better cache locality. " -- https://github.com/llvm-mirror/llvm/commit/7ffec838a2b72e6841d9fb993b5fe6a45f3b2a90

"

masklinn 18 hours ago

According to https://github.com/Microsoft/clang/blob/master/docs/SafeStac... safestack alone doesn't fully protect against ROP:

> With SafeStack? alone, an attacker can overwrite a function pointer on the heap or the unsafe stack and cause a program to call arbitrary location, which in turn might enable stack pivoting and return-oriented programming.

And you need additional features (such as CPI from the paper you and the commit message link to) for full protection.

reply "

moyix 15 hours ago

From the paper:

> This is because objects that end up being moved to the regular (unsafe) stack are usually large arrays or variables that are used through multiple stack frames. Moving such objects away from the safe stack increases the locality of frequently accessed values on the stack, such as CPU register values temporarily stored on the stack, return ad- dresses, and small local variables.

I wonder if this speedup effectively hides the performance overhead of SafeStack?.

reply

 extropy 12 hours ago

Why don't we have a CPU architecutre with two stacks - one for stack data and another for return addresses?

reply

MichaelGG? 8 hours ago

Or write code in languages that, you know, don't encourage unwanted arbitrary code execution?

reply

arielby 6 hours ago

That's what SafeStack? (and IA-64) do.

reply

---

glacambre 12 hours ago

link flag

Provability is starting to matter more and more. There are very big companies getting involved in that space - Nvidia has started using Spark, Microsoft has been funding work on things like Dafny and F* for a long time, Amazon uses TLA+… Provability is just getting started :).

--- " Verification

RedLeaf? provides a Floyd-Hoare-style modular verification (i.e., based on pre-conditions, post-conditions, and loop invariants) for low-level systems that are designed to be fast and small. It achieves that by developing a new verification toolchain built on the SMACK verifier, Boogie intermediate verification language, and Z3 SMT solver. " ---