A few years ago I started researching on Software correctness. I was actually interested in software security, but I was unaware of the difference at the time. Now, after researching in both areas I can finally discuss the difference between those two concepts.
What does it take to mathematically define if a specific program is correct and/or secure?
Fist I will talk about correctness, then security.
We say that a program is correct if it respects its specification.
Thus, it does not even make sense to talk about the correctness of a program on its own. Correctness is actually a consistency property of a pair program + specification.
Let's consider a very simple program with a simple specification:
//Post: the result is a positive number
int foo(){return 5;}
Is this code correct? That is, is it true that the result of calling that method will always respect the specified post-condition?
Well... NO. For no real architecture that method will always return a positive number. In some situations calling that method will simply raise a StackOverflow error, and sometime the physical hardware will crash and burn before being able to compute the result.
However, most developers would agree that the code above is correct, or at least, as correct as it can possibly be.
That is, we are not considering correctness in an absolute sense, we are considering a simplified execution model with certain simplifications with respect to the hash reality, where anything can fail at any point anyway.
Many researchers in the area of software verification seams to simply accepting that there is going to be this set of simplifications that hopefully will be irrelevant in most real life situations an focus on mathematically modelling code execution in order to prove correctness (that is, consistency between code and specification) on such a simplified execution model.
Instead, I decided to study and categorize those simplifications:
If we can not make proofs on the actual execution model, what execution model should we use?
I say that an execution model more close to reality has a bigger scope that an execution model that excludes more difficulties.
Most of the verification for correctness research area works under the following simplifications:
1.-No StackOverflow: we assume we have an infinite stack
2.-No MemoryOverflow: we assume we have an infinite heap
3.-I/O control: we assume no other process is editing our files
4.-Uncorrupted Root: we assume other processes can not randomly edit our memory bits
5.-Correctness of the OS: OS functionalities behave as expected
6.-Good Hardware: we assume no HW bugs
7.-Small Physics: no cosmic ray bit flips or funky quantum events
8.-Large Physics: no power cuts, no explosions or kicks to the HD
9.-Deployment: the code we checked is the one that will actually run
(Disclamer, my experience is mostly on OO verification)
Definitions
Thus, under those simplifications we can define Correctness as follows:
A program is correct if it always does the right thing
Where the specification identifies what is the acceptable range of right things.
Now we can contrast the definition of correctness with the one of
Security:
A program is secure if it never does the wrong thing
Warning: the scope is implicit.
At a first glance it may look like security is simply a subset of correctness. However, the SCOPE is often different.
When discussing about security we do not accept simplifications 1, 2 and 3; that is, even if there is a StackOverflow, we still can not accept to perform an invalid action.
In response to a StackOverflow it is ok to crash , but it is not ok to send our private information to another country.
Thus, usually we attempt to verify correctness under simplifications 1-2-3 and security without simplifications 1-2-3 (but still with simplifications 4-5-6-7-8-9).
In particular, without 1,2 near every program is simply incorrect.
While 'the right thing' is often defined using pre/post conditions in some logical framework, 'the wrong thing' is often defined using actions: we abstract over the internal state of the program and we just observe the interaction the program has with the rest of the world. Usually we can represent those interactions as forms of I/O or calls to low level OS functionalities.
Under this lens, terminating the program with an error message is often not considered an action. Going in loop is also often not considered an action.
(Models of security focusing on a unit of code often do not model Denial Of Service vulnerabilities; they are better addressed considering multiple processes running together, and thus out of scope for this discussion).
To further clarify the difference of security and correctness, consider the two examples below:
An universally secure(but not correct) solution to any problem
throw new Error("NOPE!");
That is, we can simply refuse to act. No action means no security violation.
An universally correct (but not secure) solution to any problem
Assuming to have a function correctlyDoStuff(..) that is both correct and secure, we can forge a correct but not secure version of it:
int doStuff(int x){
try{rec(aNumber);}
catch(StackOverflowError o){ badAction(); }
return correctlyDoStuff(x);
}
void rec(int i){ if(i==0){return;} rec(i-1); }
where badAction does a security violation, like formatting the hard drive.
For any real execution environment of our code for our doStuff function, there exists a number aNumber that will trigger the StackOverflow, but in the verification for correctness model, the catch is recognized as dead code.
Indeed, some code verification tools will accept such a solution as correct.
Conclusions
There is a lot of confusion between correctness and security.
I hope I clarified the terms a little bit here.
Ultimately, there can not be full agreement on any terminology, but if we want something that can be mathematically modeled and checked/verified, the introduced terminology is a very good starting point.
Also, terminology in this area is so challenging that I do not think it is fair to require developers and companies to have a good grasp on those terms.
In particular, if you/your company want security and someones tries to sell you correctness without making sure that you understand the difference between the terms, they may be scamming you.
Overall, in my opinion we should start by writing SECURE software, and only after we are certain that we are well rooted in a secure environment we should start working toward CORRECTNESS.
Latest comments (0)