Welcome. In this session, we will learn about some properties of programs that we would typically check using static analysis. So one way to think about these properties is to think about the complexity of analyzing programs for those properties and classify the properties accordingly. So they could range from very simple properties to very complex program properties. At the easy end is what we could consider syntactic properties. These are things like naming conventions, file naming rules. Things that a typical linter would check. These do not require too much sophistication to check, but at the same time they do not tell much about the program. We can think of these properties as enabling other analysis. For example by humans when they are reviewing the code, it would be helpful if certain naming conventions are followed. For example when I read a variable name, if there is some information that consistently tells me what its type is, what its range is, and so on, that would be helpful when we're reading through the program and understanding its behavior. Next could be simple semantic properties. Like value ranges are typical type checks that we do in programs, whether a variable and the expression that it's assigned to has the same type. These are typical checks that are done by compilers. It doesn't require too much of contextual or flow or path information. It analyzes the program based on some information annotated with the data that's in the program, and check some basic things. Again, your type-correct program need not be correct in its behavior but if it's not type-correct, it's not even going to compile, or if it's a dynamic language, we may see some run-time issues. So, avoiding certain kinds of issues like that can be done with simple semantic checks. At the next level what we would consider are flow-sensitive properties. These are the typical data-flow analyses that we saw. So here, the idea is we reason a little bit deeper about the structure of the program to look at its control-flow graph, and check for properties that depend on whether those are paths on the control-flow graphs or not. For example, whether the definition and use are potentially linked can be determined by looking statically at the control flow graph for the program, and seeing if there is a path from the potential definition to use without any intervening definitions. Then we will declare, "yes, that is a potential def-use relationship." The actual def-use relationship may not materialize because the path conditions may not allow that path to be really executed in any possible execution. So, to determine if there is an actual def-use relationship, that's a path-sensitive analysis. We would have to take into account the constraints on the path that determine whether the path executes or not. And if it executes, under what conditions. So, these kinds of analysis, it could be done at a pretty modular level. We can look at the single procedure or a single class and analyze these properties. But to reason about whole programs, it's not sufficient to only consider paths, but we should also consider the context. In other words, when a function is called, in what calling context is that function called? For example let us say we want to look at a program and determine whether there is any possible null pointer access in a program. Now, if we have to precisely determine that, we need to understand all pointer accesses, and the context in which the pointer access would happen. If a function is called, which does a pointer access and it is called from ten different locations, we may have to analyze each of those contexts to see if the pointer could be null or not to be precise. Of course, we would often substitute such precise analysis with simpler but easier to do analysis. And so this is where the complexity of analysis comes into play in terms of classifying various kinds of properties that we use to check the program statically. Now, why do we use a range of properties? As we saw earlier, program properties of interest are in general undecidable. That means, any automated analysis for any interesting property will necessarily misclassify some programs. It may say "yes" for some when it shouldn't and it may say "no" for some when it shouldn't. In other words we cannot have an automated procedure to do that. So as a result we have to always do some approximation and have human-in-the-loop to pass judgments about the programs. So to help the human-in-the-loop make the judgement effectively, we need to look at the analysis and see what kind of trade-offs we have to deal with. Typically, all analysis involves some trade-off between precision and scalability. So, simpler analysis not very precise information which may give some useful information but it may scale to larger programs. On the other hand very precise analysis could be very powerful but it could not, in practice, scale to programs that are large, that are typical software systems. So, too much loss of precision makes the results useless and precise analyses are too complex to scale up. So, the humans involved need to make the right trade-offs and so we need a range of these properties that the people analyzing the program can try and choose the appropriate ones for the software under consideration. So, to make the automation useful, we need a range of such properties. Another way to classify this analysis is based on the kinds of approximations in the analysis too. We have already said that every analysis has some imprecision that is going to be some approximation. So, one way to think of it is whether it's a "must analysis" or a "may analysis". What we call a "may analysis" is an approximation in which the analysis makes an over-approximation of the program behavior. In other words, the analysis is going to consider some potential behaviors that may not actually be feasible in the program. As a result, if the analysis proves a property, that is it shows there are no null pointer accesses in a program based on the over-approximation of the program behavior, then we can be certain that that property is true. On the other hand, the bugs detected may be, really, false alarms. It may over-approximate the program and say, "Hey. Here is a potential path where that could be a null pointer access." And on closer scrutiny, we may determine that's not the case. So this is really the place in which the human has to come in and say, "I looked at this program and even though this is an alarm, it's a false alarm and classify it as not an issue." So too many false alarms can actually make the analysis quite useless. On the other hand, "must analysis" under-approximates the program behavior. So it considers only a subset of program behaviors. So in this case, if you want to be sure that the bug is present, we want a concrete evidence of an actual feasible path in the program in which the bug will manifest, then a "must analysis" will do that for us. On the other hand, we may not be able to establish any properties. Just because a "must analysis" said there is no out-of-boundary access, it doesn't mean that there is no out-of-boundary access because it hasn't looked at all possible behaviors. Why do we need this range of properties or different kinds of properties? How do we use it? Here is a typical scenario. We take the software and usually as part of the software development process, each organization or each software development environment will have its own set of processes to follow. One of that would be to have the software go through some static checks. Simple static checks like lint. So that coding conventions are obeyed. Some basic rules about code such as MISRA C's rules are followed and so on. And these could become your gating conditions before it's given to people for review. And then there'll be typically certain common but more sophisticated analysis that are run to check for potential issues like memory access issues, program crash, and so on. Usually these analyses introduce some kind of imprecision and the results are typically reviewed by actual developers or analysts to see if those are real issues or not. And in certain situations, we may have very project-specific analysis. Maybe it's a security application, we want to have several types of analysis to check if there is a potential information leak or tainted data flowing into locations where there should be untainted data and so on. And we may have those project-specific analyses also run on the software. Typically, these become more sophisticated and as a result, there is something like the false positives that show up, basically false alarms that the reviewers have to then look at and determine whether the analysis is reporting a real issue or not. In all of these, there are little tuning knobs in some sense to select how precise we want and how much we want to scale depending on various factors like whether we have to consider flow sensitivity, whether he have to consider path sensitivity, whether we have to consider context sensitivity or not, and what kinds of data abstractions are introduced, and those can determine the actual rate of false positives and also determine how scalability analysis is. These factors have to be taken into consideration when static analysis tools are put into use in product development.
