From: Harvey Newstrom (mail@HarveyNewstrom.com)
Date: Sun Jun 13 2004 - 10:42:23 MDT
On Sunday, June 13, 2004, at 03:37 am, Samantha Atkins wrote:
> I don't see how "formal verification of Java programs" can be done.
> Or at least, I would assume that the specification of what the program
> is supposed to do is where much of the trick takes place.
There are formal techniques for verifying, or at least, reviewing and
checking whether a program is doing what it should. "Safety", or in my
field, "Security" is much harder to do because it deals with "aspects"
of a system. An "aspect" is an emergent property of a system that does
not derive from any particular Java object. Even if every object does
everything exactly right, the overall system may not be safe or secure.
This is where Information Assurance comes in. It involves testing,
review, auditing, and all sorts of processes that most developers never
do in a formal way.
> If the specification is detailed enough and is itself provably
> correct (why don't we get an infinite recurse?) then it might well be
> a better form of the program than the Java one was anyway. The
> things Java removed from C++ do not afaik make it any more powerful,
> certainly not more succinct, and arguably no easier to prove a program
> is correct in.
You are exactly correct here! Java is a high-level language (or a
medium-level language according to some people). It still compiles
down to the same machine code that C does. What this means is that the
differences between C++ and Java are merely at the human readable
abstraction layer. These differences do not exist in the executable
binaries themselves. Security people often run into these "gotchas"
where Java programmers can't understand how they are getting the same
errors as C programmers:
- Pointer errors. Just because Java doesn't show pointers to the
humans in the syntax layer does not mean they don't exist. Just as in
C, Java can get pointer problems. Make a string (which is really a
character array) called A. Give it a value of "This is A". Assign B
to equal A. B is really a pointer to the same physical memory space as
A, even though Java hides this from you. Change B to "This is B".
Guess what value A has in it now? Yep, it says "This is B". A C
programmer expects this. A Java programmer does not.
- Similarly, Java can abort with null pointer exceptions, even though
the syntax language does not define pointers, the compiler does.
- Java does garbage collection for you, so the language doesn't provide
this feature. This just means that Java doesn't control it of
understand it, not that it doesn't have it. Java will fill up memory
until it runs out, and then the entire program freezes while garbage
collection occurs. The program will continue after a brief pause.
This makes Java unacceptable for real-time or critical operations,
because it can unpredictably freeze in an uncontrolled manner where C++
can be controlled.
- Also Java security is at the syntax layer. You can define an object
class to be private, and the compiler won't let other people access it.
But the executable doesn't do this. Binaries can read anything they
want and will not get the compiler error. Also, the compiler only
forbids it if your header files tells it to. If you redefine your
PRIVATE to be compiled as PUBLIC, you can access anything you want. To
a security person, there is no Java security. The Java protections are
suggestions only and are not enforced or controlled. For auditing
purpose, these are not controls.
Just some nitpicks, to show where things can go wrong in the final
system that are not detectable in the individual objects or from the
source code. Every object can function perfectly, while the entire
system fails. This is where security and safety become difficult to
enforce.
> I believe you can do this type of formalism for fairly small
> programs. If it works for larger software systems then your friends
> should practically own the server software space.
People like me try to do this formal assurance for large systems. My
new job in Washington DC is as Principle Security Architect for the
National Archives and Records Administration. It is my job to define
the architecture that will keep government records safe. This even
includes classified records. It is huge and it does require formal
assurance that will take years. Security, Assurance, and Safety must
be full-time jobs within the design team from the beginning, or else
the system won't be secure, assured or safe.
-- Harvey Newstrom, CISSP, CISA, CISM, IAM, IBMCP, GSEC <HarveyNewstrom.com>
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:47 MDT