Formal verification creates hacker-proof code


#1

#2

I wonder if SAFE’s code could be written like this?


#3

A few points

  • Note the use of “were unhackable with existing technology”

  • One reason for going to RUST and minimising conditional clauses was to assist in doing “formal verification”. Compared to C, RUST is magnitudes easier to formally verify.

  • This has been around for 30 years or more. I learned it in Computer Science classes at UNI in the 70’s

  • The example given while complex enough is control system programming which is essentially mathematical so its algorithm is mathematical and the code should be executing this algorithm. So its well suited for this 100% proof. Other systems are not so easy and often can only be partly done because the mathematics is too complex.

  • SAFE code is a combination of systems, some protocol and easier to mathematically prove and others more decision making and somewhat harder.

  • The example in the article was for a single purpose system whereas the interaction between subsystems is often where hackers get a foothold. This is also going to the major headache for SAFE code to formally verify, the interaction between protocols and subsystems.

  • Many hacks don’t involve the code that is being written. This means that even though the code is perfect and passes 100% the formal verification it could still be hacked. For instance a buffer overflow in the underlying OS (OR DMA controller) can inject code into the application thus negating any amount of verification done on the code.


#4

How is the interaction between subsystems of the SAFE code?
I had some fairly good experience with Contract testing (Consumer-Driven Contracts: A Service Evolution Pattern), if the interaction is made thru APIs (e.g. RESTful) perhaps it can be considered.


#5

I was considering the interaction between the network layers, various modules such as routing, crust. Also the interaction between various personalities of the nodes. This is where the work of defining precisely the all the conditions that can happen in the protocol, does each module using the protocol interact with the protocol the same way (understand the protocol states precisely the same).

It is one thing to have all modules interact correctly (mathematically proven) when using a particular communications protocol, but do all modules interpret/“understand” the protocol the same? That is a simple example, but when you have a number of communications occurring for a module, does the order of packets affect the module one way and the sending nodes expected another effect. Race conditions can occur, such as two nodes trying to update an SD object at the once address. If the nodes handling the SD object do one thing yet the sending nodes expected another (say error messages) then issues arise and the effectively the whole network has not been proven, even though it may still work correctly.

So its not like its too difficult, but when you are running a full network as compared to a singular control program the complexity increases dramatically. And this is on the core network side of any APIs to the client s/w, which is another set of things needed to be proven.

I expect for the current development that formal verification of modules is feasible, but traditional testing of the protocols will ensure.


#6

Thanks for your detailed explanation @neo, even that Contract testing contemplates a precondition/pre-state of a node/subsystem for testing an interaction, I don’t think it can be used for testing those interactions since it seems you need to verify many combinations of pre and post conditions.


#9

Part_01 of my comment that is split up due to the 2-links-per-post limitation.

What regards to formal verification, then the main author of the Pentagon programming language, Ada, Tucker Taft, has created a brand new systems programming language,

(comment continues)

Part_02 of my comment that is split up due to the 2-links-per-post limitation.

ParaSail (parasail-lang.org), which has the following features:

  • Formal verification tools come with the compiler. Newest version of the compiler uses the LLVM.

  • The maximum value of the Integer type is limited only with RAM size.

  • Totally new threading model: auto-parallelization is part of the language semantics and implementation, id est the same code that can take advantage of 2 CPUs, can take advantage of 1024-CPUs.

  • No legacy dragged along. The project started as a hobby project of the Tucker Taft and everything is developed mainly by him and really FOR QUALITY, NOT DEADLINES. ParaSail is meant to be the language that is used in the future avionics, nuclear reactors, medical equipment, all other safety-critical systems that benefit from a system programming language.

(comment continues)

Part_03 of my comment that is split up due to the 2-links-per-post limitation.

I am NOT a ParaSail developer. I do NOT have any formal association with ParaSail’s original author, Tucker Taft. I’m just a fan of his work, who has re-packaged his work (with his help at his ParaSail forum). My version differs from Tucker Taft’s (id est the upstream) version mainly by the fact that my version is tailored for servers and robots, while the Tucker Taft’s version builds/compiles only, when GUI-libraries are available. (He told me at his ParaSail forum, how to outcomment the GUI library dependencies.)

(Due to the 3 posts per thread limit for new users my comment continues at my site.)