Now we're going to dive into some details of the
implementation of this program. Let's look at
the actual implementation of the login program. Now, when you're doing
this using formal methods, you basically prove your programs are correct, and by program, I want to emphasize
I mean source not executable. You formally state
your assumptions in your operations and then you
prove that for each routine, if the assumptions on
entry are correct, then the output or the results is going to be exactly
what you said. So, let's take a look at
some of the example proof, and this is a formal one; we're simply going to
compute the remainder of x divided by y. You can see the function written
there, it's very simple, it's in C int rem of int x, int y while y is greater than x, x minus equals y
and then return x. So this is not using
the remainder operator. This is actually doing it the hard way, repeated subtraction. Okay. So the assumptions
we're going to make initially are x's and y are
greater than zero. Why? Because if it's negative, then the line in the y loop is going to cause
all sorts of problems. So let's just assume that
for the precondition. Now, we get to the while loop. If we enter the while loop
at this point, we know x and y are
both greater than zero and x is greater
than or equal to y. Then after we subtract y from x, we know that x minus y is
greater than or equal to zero and then we have x is greater than zero and
y greater than zero. We continue doing
this until finally x is no longer greater than y and then we go to the return. So, on exit we have
the following, x is greater than zero and
y is greater than zero. The value that's returned, which is represented here as R-E-M is also greater
than or equal to zero. It's also less than y. The reason for that is
because you continue looping until x is greater than or equal to y is
false to follow the y loop, so now the x you're
returning is less than y, and the x you returned
is represented by rem. So that's where the rem is
less than y comes from. Then the last part says that, rem is simply the remainder
of x when divided by y, and that's very easy in
a mathematical sense rather than a computer science sense. It would have used
a triple bar equals instead of a double bar equal
to emphasize that this is mathematically rem
is congruent to x mod y. So now let's apply
this idea to the login. What are the
preconditions to login? Well, login is going to
export environment variables, so that means we're going to have to assume, or rather check, that no environment variables
have string length over 1,024 characters because that can pose problems to some shells. If it's an empty or no value, don't export it and don't
export anything named in a list of specific
variables not to export. The post-condition
for environment variables is that in fact, the environment
variable is placed in a list of variables to be
made available to the user. So we're going to focus on this. There are other preconditions and post-conditions as well, but we're just going to focus
on this in the interests of keeping this to
a reasonable length. So let's look at
the export function. This is the one we're
talking about here. Again, it's local to
login and you give it a character string
that represents the environment variable,
A equals value. What this does, is
it returns, one, if you should be able to
explore it, if it's exported. In fact, it always returns one. First of all, it looks to see
if there's an equal sign. If it finds an equals sign, it replaces the equals
sign with zero. So now we have a null value. We then add it to the list
of things to be exported. We have s, which is the
environment variable name, p plus one which is the value, and one meaning that yes
it's to be exported. Then since the program itself may rely on that
environment variable, we return the equals
sign to where it was and we return success. Question, what's the flaw? Well, suppose the
environment variable doesn't have an equal sign? Then it's defined
but it has no value. In this case, what will happen
is strchr which finds the first equals sign from the beginning of
the string will return no. The next line will dereference a null pointer
and the program will crash. So you don't want that. So now what we're gonna do is check all the preconditions. So here's another version of export that does all sorts
of preconditions. By the way, the export on a previous slide was from an old version of
the lock-in program. First thing we're going to
do is check to be sure that the string length is
not greater than 1,024. Notice here we return zero
if it's not to be exported, and one if it is unlike the previous routine
which always returned one. The next one is, we looked to see whether or not it's got a value; if it's just the variable name, meaning it's set but has no value, we don't
want to pass it. So the first thing we do is check to see if there's
an equal sign in it. If there is, we immediately
return continue. If there's not, we immediately return a
zero because we're done. Let's look at handling
precondition three. We have a list of elements
not to be exported, that's the variables
and no export, and it's just the list
of environment variable names not
to be exported. So first we get the length of the environment variable name, then we look at the thing
we're checking, which is s and see if there's an equal sign
there at that position. If there is not, then it's not the right variable
and so we just skip. If it is, now we have to see whether or not
that variable name, the name of what we're looking
at is not to be exported. So, we compare the
characters from zero all the way
up to the n minus first and see if that matches what's in the null export element that
we're looking at. If they do match,
then strncmp zero and we return zero.
So we do that check. So now we've checked
the preconditions and then we stick
the original code in there, which you can see, and now
we check the post-condition. We look at the value of setenv. If that failed, then we return zero otherwise
we return one. Now what's interesting
is when I did this, I got curious and I looked
at the FreeBSD login code. This is much more modern than the export code I
showed you earlier. It turns out they do exactly
this precondition checking. The only thing they
don't check is the post-condition to be sure that it made it into the list and there
wasn't a problem. So, this shows that
systems are moving towards a much more secure
system programs. But it also shows
how valuable this is because it shows
that FreeBSD people, who are very security
conscious took great care. So, what are the lessons of this? First, know your assumptions, check them whenever
possible and if you can't, look at the results, see if those make sense. Don't expect system calls or library functions to do what
they don't claim to do. In other words, if it doesn't
say it, it doesn't do it. You may know somehow through experience that it
does, don't rely on it. In the 1960s when IBM
360s were being marketed, people found all sorts of undocumented instructions
and relied on them. But the undocumented
instructions were also often changed
in the next release, because since they were
undocumented, IBM said, well, we can make these meaningful and do something or changed
them and have something documented and it messed
up a lot of people. Same thing here. If
the library functions descriptions don't say it does something, don't
assume it does it. Also read the fine print. If you look at SGRN copy, you'll think, "Well, geez, it'll copy up to n characters." Then see in there it
will put a null byte at the end and in fact, it will copy up to n characters, but if the length of the buffer you're copying into
is n, in other words, it stops because it's
copied n characters, there'll be no null byte,
so you have to add it. Finally, the next checklist, are your goals well-defined? Well, with login they
were and we know that because we wrote them out
and worked through them. Point of fact, in
high assurance programming, you would need
even more specific goals, but these were good for
ordinary programming. Did we check our assumptions? Well, you saw what
we did with export, we would be doing
exactly the same thing with the other components of login. Then, when you have operators, are you share the values
are meaningful? For example, if you're
doing remainder, are you sure that
both numbers are positive and the
dividend is not zero? If you're doing
a division, makes sure that divisor is not zero. If you're going through
an array using plus plus the increment one, makes sure that you don't de-reference one beyond
the end of the array. Always check that you're not
beyond the end of the array. In fact, the pointer
can't have a value beyond the end of
the array. That's fair. But you can't dereference
the pointer at that point. You can use this to detect when you're
done with your array.