4 ms·

>> For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. > Also, a bug in the compiler could introd

>> For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. > Also, a bug in the compiler could introduce such a bug. > To my knowledge, the major Ada compilers have a very good reputation for correctness, but none are formally verified, and there's no such compiler on the horizon. No, a bug in the compiler does not introduce such a bug. A bug in the compiler is a bug in the implementation and does not equate to a bug in the formal spec. It is rather like a fault in a machine or a building arising from a dodgy supplier using below spec materials, or a fault in the manufacturing or assembly process.

MaxBarraclough 7y ago
> No, a bug in the compiler does not introduce such a bug. > A bug in the compiler is a bug in the implementation and does not equate to a bug in the formal spec. We weren't discussing the challenges of creating a correct formal specification. I presume you meant a bug in the formally verified implementation, rather than a bug in the formal spec, in which case: More precisely then: a compiler bug could introduce a defect into the final system, which was not present in the formally verified implementation source code. (This assumes that the scope of the formal verification stops at Ada source code.) > It is rather like a fault in a machine or a building arising from a dodgy supplier using below spec materials, or a fault in the manufacturing or assembly process. Those are all risks that mechanical engineers need to deal with carefully. If it's your job to deliver a defect-free avionics software binary, then dealing with the risk of compiler bugs is part of that. A company like Airbus isn't going to treat compiler bugs as Eh, not our problem. Presumably they're going to be careful in their choice of compiler, and back it up with testing. My point was that a bug in the compiler is similar to a bug in hardware, in that it opens the door to defects which are formally assured to be absent from the verified implementation's source code. It's possible to use formal verification to guarantee against issues arising from compiler bugs, it's just that I don't think this can currently be done with SPARK. There are two formal approaches to protect against compiler bugs: either use a formally-verified compiler (like the CompCert C compiler), or use a non-verified compiler and then verify the correspondence between the input source and the generated machine-code (the approach used by Sel4).

MaxBarraclough 7y ago

> No, a bug in the compiler does not introduce such a bug. > A bug in the compiler is a bug in the implementation and does not equate to a bug in the formal spec. We weren't discussing the challenges of creating a correct formal specification. I presume you meant a bug in the formally verified implementation, rather than a bug in the formal spec, in which case: More precisely then: a compiler bug could introduce a defect into the final system, which was not present in the formally verified implementation source code. (This assumes that the scope of the formal verification stops at Ada source code.) > It is rather like a fault in a machine or a building arising from a dodgy supplier using below spec materials, or a fault in the manufacturing or assembly process. Those are all risks that mechanical engineers need to deal with carefully. If it's your job to deliver a defect-free avionics software binary, then dealing with the risk of compiler bugs is part of that. A company like Airbus isn't going to treat compiler bugs as Eh, not our problem. Presumably they're going to be careful in their choice of compiler, and back it up with testing. My point was that a bug in the compiler is similar to a bug in hardware, in that it opens the door to defects which are formally assured to be absent from the verified implementation's source code. It's possible to use formal verification to guarantee against issues arising from compiler bugs, it's just that I don't think this can currently be done with SPARK. There are two formal approaches to protect against compiler bugs: either use a formally-verified compiler (like the CompCert C compiler), or use a non-verified compiler and then verify the correspondence between the input source and the generated machine-code (the approach used by Sel4).