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.