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.