12

I've read that code is formally verified by constructing a mathematical model of the code, and then a formal proof is provided to demonstrate that this model meets certain requirements. How does formal verification ensure that the resulting code is free of any vulnerability?

Improve this question

7 Answers 7

Reset to default
16

It doesn't guarantee that the code is free of vulnerability. However, if verification is used appropriately, it can increase assurance (confidence) that the application is secure.

Speaking from a very broad perspective, there are two aspects of this problem:

  • Verification. Given a mathematical model of the system and a mathematical specification of the requirements, does the system meet the specs?

  • Validation. Do we have the right set of requirements? Does the mathematical spec accurately reflect the true requirements? Does the mathematical model accurately and completely correspond to the code?

Sometimes people focus only on verification, but both matter.

In your situation, if the specification incorporates all relevant security requirements, and if the mathematical model correctly corresponds to the code, and if the verification is done appropriately and is successful, then we may have a basis for significantly increased assurance that the system will meet our security requirements.

In the best case, verification can be a powerful tool to help assure security, one of the most powerful that we have. However, as with anything, it is possible to misuse the technology or get a false sense of security if it is not used appropriately. One of the most common failure modes is that the verification process does not verify all relevant security requirements (some are overlooked or omitted).

To say much more might require delving into the details of the system, the security requirements, and the nature of the verification that was done, but hopefully this gives you an overview.

Improve this answer
1
7

Formal verification does not guarantee a secure system. Nothing guarantees a secure system. What formal verification can do is provide a very high assurance that some parts of the system are secure.

Formal verification gives a mathematical proof that under certain assumptions, a model of the system has certain properties. Thus, if part of the system has been formally verified, there still remains several conditions for the system to be secure:

  • Are the assumptions underlying the verification met?
  • Does the system match the model that has been verified?
  • Is the proof given by the verification system correct?
  • Are the proven properties sufficient to ensure the security of the system?

The extent of the formal verification can vary a lot. For example, buffer overflows — a common kind of vulnerability — can be spotted pretty easily: most languages that are higher-level than C or C++ guarantee the absence of buffer overflows in the compiled program. It can nonetheless happen that the compiler allows broken code to get through — while compiler bugs are a lot rarer than program bugs, they are not impossible. Buffer overflows are only one kind, however; most systems' security depend on far more than knowing that there are no buffer overflows. (Related reading: Why don't computers check whether there are memory contents in some memory space?)

To illustrate the limitations above, let me take a concrete example. Some smart cards run a Java Card virtual machine, and execute only bytecode that has been verified. The bytecode verifier, in principle, guarantees that the code cannot peek or poke outside its alloted memory space. This avoids some vulnerabilities but not all:

  • The verification only guarantees its properties if the bytecode interpreter behaves according to its specification. Furthermore, if hardware does not execute the interpreter correctly, all bets are off (for example, one way to attack a smartcard is to cause a power glitches which results in some instructions being skipped).
  • If there is a bug that allows code to be uploaded without going through the verifier, then it is possible that the code on the card will not have the properties guaranteed by verification.
  • The verifier itself may be buggy and allow incorrect code to be uploaded.
  • Even if the code of the applications on the card does not directly access the memory of other applications, it may still spy or perturbate them in other ways. For example, it may exploit a side channel such as timing to deduce properties of other code running on the same device.
    Furthermore, the security of the system may depend on things other than the isolation between applications on the card. For example, the authentication system may allow an attacker to take control of the card, there may be a protocol-level vulnerability that allows the attacker to disrupt communications, etc.

In a high-assurance system, formal verification can help in two ways:

  • Proving that the code matches its specification. This requires a formal model of the execution environment (hardware, compiler or interpreter, standard library, …) and a lot of work.
  • Proving that the specification has certain desirable properties. This requires a formalization of the specification, a judicious choice of properties and a lot of work.

The Common Criteria for security evaluations define several assurance levels. Only the highest assurance level (EAL7) requires formal verification. This is not the only requirement: formal verification does not preclude the evaluation of other aspects of the system, including documentation, penetration testing, etc.

Improve this answer
3

Formal verification really only works in extremely constrained cases where a system can be modeled as a series of transforms with clearly defined domains, ranges, and clearly understood rules that define the behavior of a function - in many cases this means that you're dealing with a system that is the software realization of a mathematical model, or that it's (relatively :-) ) easy to derive a model from the systems behavior (digital circuits of significantly less complexity than a general purpose CPU)

I worked in some forerunners to this in the '80s, where the effort was in generating 'provably correct code' - One system I recall was named Adele, and operated on programs written in (uggh) Ada. Anecdotally, we used to joke that using Adele meant that it took 10 times as long to write, it ran 10 times more slowly, and it only crashed 10% as much - You might want to look at Bertrand Meyer's writings on Eiffel, he put significant thought and effort into how a language could provide internal verification checks via preconditions, postconditions, invariants, and a bunch of other stuff I have since forgotten.....

Improve this answer
3
  • According to the 2nd link I gave in my answer, in 2009 a general-purpose operating system kernel was verified. IMHO that might not be considered to be an extremely constrained case in view of the spectrum of functionalities that the kernel has to provide in realtime.
    – Mok-Kong Shen
    Oct 11, 2012 at 19:16
  • You're looking at second order effects - you can verify that a loader provably performs a transform,e.g. the source memory array ends up in the destination - proving that any code it loads does not in fact render the system unsafe is outside of scope - and that's less than 10K lines of >microkernel< taking 200K lines of proof to prove - some things never change :-)
    – Mark Mullin
    Oct 11, 2012 at 20:57
  • Actually, that's inside the scope. The scope is an isolation kernel with control of CPU, memory and IPC flows. Such a proof shows that, with certain restrictions on the code, anything it does won't render the system unsafe beyond that code's partition. Proving more than that requires more effort. Which is the point of isolation kernels: you only pay for what you use in the final system.
    – Nick P
    Jul 14, 2013 at 19:05
2

Verification checks to see if the system has a specified property. Properties maybe expressed in various notation and logics. Specifying these properties is difficult. So if a designer can express their idea of security in a formal notation suitable for verification, and the software is proven to satisfy the property, then yes it is secure. In real life, its almost an impossible goal to verify non-trivial properties on real software running on general purpose hardware

Improve this answer
1

Any vulnerability is too broad a term, since formal verification (in effect automated proof that an algorithm/system possesses specific properties) is geared toward specific threats: sensitive data leaking out, external information percolating through the defenses, memory leaks, allocation blunders, stack overflows etc. For some preview of current work in this regard you can e.g. visit Software Engineering Institute at Carnegie-Mellon Uni.

Improve this answer
0

Formal verification checks only conformance of coding to given specifications. If a specification itself is improper/incorrect, then an eventual verification is evidently of no value. For informations on formal verification see e.g. http://en.wikipedia.org/wiki/Formal_verification and http://en.wikipedia.org/wiki/Isabelle_%28proof_assistant%29

Improve this answer
-1

Any model couldn't guarantee a secure, error free code. Only continuous testing can give you temporary security. Finishing a code doesn't mean that it will remain secure, so further continuous testing against new vulnerabilities required.

Improve this answer
7
  • 1
    I'm not sure that this is a correct characterization of formal verification. If you can formally prove the code is secure, then continuous testing is redundant. Perhaps you could provide some citations to illustrate how vulnerabilities could appear in formally verified code?
    – MCW
    Oct 12, 2012 at 11:09
  • New attacking vectors can reveal new vulnerabilities in formally proved code also.
    – sh4d0w
    Oct 29, 2012 at 15:35
  • Could you substantiate that?
    – MCW
    Oct 29, 2012 at 21:31
  • Not so much evidence required as a lot of vulnerabilities have a proof-of-concept code. Those codes were also formally proved but after some thinking, somebody could find a way to hack it - there is no invulnerable applications out there.
    – sh4d0w
    Oct 30, 2012 at 12:13
  • I'm unfamiliar with a single example of formally proven code being demonstrated to be vulnerable. I'm not sure that we're using the term "formally proven" to mean the same thing.
    – MCW
    Oct 30, 2012 at 12:22

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .