# Security and Dependability Aspects

---

###### tags: `NCKU`, `lesson`, `splint`
---
## Revision record

| version | comment | author |
| ------- | ------------------------ | -------- |
| v0.1.0 | document built | Marco Ma |
| v0.1.1 | 16.1 and 16.2 update | Marco Ma |
| v0.1.2 | section Annotation added | Marco Ma |
| v0.2.0 | reference list added | Marco Ma |

---
## Outline
* Introduction
* Annotation
* 16.1 Introduction to SPLINT
* 16.2 Basic Checks
* 16.3 Memory Management
* 16.4 Buffer Overflows
* 16.5 Function Interface Annotations
* 16.6 Summary

---
## Introduction
Splint is a static code analysis tool, it could detect problems like memory leak, null pointer, buffer overflow, etc.

## Annotation

| Annotation | meaning |
| ------------------------ | -------------------------------------------------------------------------------------------------------------------- |
| ```/*@only@*/``` | the pointer is the only one which pointed to the data |
| ```/*@owned@*/``` | pointer has responsibility to free the storage it points to |
| ```/*@dependent@*/``` | the object might share by mulit pointer, in other words, pointer doesn't have the responsibility to free the storage |
| ```/*@in@*/``` | the value is completely defined |
| ```/*@out@*/``` | the value might not completely defined |
| ```/*@requires@*/``` | the condition following must be true before the function start |
| ```/*@ensures@*/``` | the condition following must be true after the function return |
| ```/*@maxSet(buf)@*/``` | ```char buf[MAXSIZE]``` we have ```maxSet(buf) = MAXSIZE - 1``` |
| ```/*@maxRead(buf)@*/``` | highest index for buf which has init already |
| ```/*@modifies@*/``` | list which variables a function may modify |
| ```/*@special@*/``` | argument handle with further annotation |
| ```/*@uses@*/``` | function has read permission, argument defined before function start |
| ```/*@sets@*/``` | function has write permission, argument memory allocated before function start and defined before function end |
| ```/*@allocates@*/``` | function needs to allocated memory for this argument, error if memory allocated already |
| ```/*@defines@*/``` | function needs to allocated memory and defined this argument |
| ```/*@releases@*/``` | function needs to release memory for this argument |

---
## Outline (Tseng)
:::info
1. Introduction
- what is static code analysis?
- why the static code analysis is popular in Embedded System?
- what's the downside?
- Static code analysis contain a lot of false positive
- others
- how to achieve?
- step 1 2 3
-

3. Basic Checks
- annotation and flags
- 4 examples
- NULL pointer
- enumerated data type
- boolean data type
- control flow

4. Memory Management
- pointer issues
-
:::

## 16.1 Introduction to SPLINT
### goal: introduce 1. static code analysis, 2. SPLINT

Basically we use ***flag*** and ***annotation*** to control SPLINT.
Where flag is defined in terminal:

And annotation is defined in code:

We use ```+``` to turn on a flag, and ```-``` to turn off a flag.
Also, we could use ```=``` to reset a flag to default or specified a value.

- What is static code analysis?
- check the your program on source code level
- check your source code through some "annotation" which was marked by programmers
- static code analysis won't execute code, in other words, this tool don't need the runtime support and OS support.
- Why the static code analysis is popular in Embedded System?
- It's lightweight and no OS/platform dependency
- What's the downside?
- Static code analysis contain a lot of false positive

---
extension:
1. scale approximately linearly with the size of the program
2. Because of 1., full interprocedural analysis is expensive, instead, each **procedure is checked independently**
3. through detailed interface information which includes the parameter and return value, global variables

step:
1. get the annotation
2. check function body with annotation (check: return value, parameters, global variables used by the function)
3. after 2., be assumed to be true (mark? annotation to true?)

---
## 16.2 Basic Checks

### NULL

### enum
enum is a datatype, for example:

enum Action{stop, sit, stand, walk, run};
//where stop = 1, sit = 2, stand = 3, etc.
Action action = stop;
printf("%d\n",action);

action = walk;
printf("%d\n",action);

action = stand;
printf("%d\n",action);

the output would be:

1
4
3

/*@ -enumint @*/
Action action = 1;

Result in having warning ```Variable action initialized to type int```

### Summary:
Introduce some basic checking, for example:
1. NULL pointer
2. enumerated data type
3. boolean data type
4. control flow




| Flag       | Effect |
|:---------- |:------ |
| useder     | When set, it enables checks concerning the use of a location before it has been initialized |
| mustdefine | When this flag
| impotus | 
| charint | 
| charindex |
| enumint |
| enumindex |
| booltype |
| predboolptr |
| predboolint |
| predboolothers |
| eval-order |
| casebreak |
| misscase |
| noeffect |
| retvalint |
| retvalbool |
| retvalother |
---
| Annotations  | Effect                                                                                                                                                                                                       |
|:------------ |:------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
| null         | Applies to a pointer and states the assumption that it may be NULL                                                                                                                                           |
| notnull      | Applies to a pointer and states the assumption that is cannot be NULL                                                                                                                                        |
| relnull      | Relaxes NULL checks for the pointer it refers to.                                                                                                                                                            |
| nullwhentrue | This annotation is used for functions that check whether or not a pointer is NULL. This annotation indicates that when the return value of the function is true, then its first argument was a NULL pointer. |
| in           | This annotation applies to a pointer and indicates that the storage reachable from it must be defined.                                                                                                       |
| out          | This annotation applies to pointer and indicates that the storage reachable from it need not be defined.                                                                                                     |
| partial      | This annotation indicates the storage reachable from the pointer it applies to, typically a struct, may be partially defined, that is, it may have undefined fields.                                         |

---
## 16.3 Memory Management
Memory Management is a major source of bugs in C programs.



| Flag           | Effect                                                                         |
| -------------- | ------------------------------------------------------------------------------ |
| stackref       | Checks about returning the address of variables allocated on the stack         |
| compdef        | Checks if a function returns a pointer to data which is not completely defined |
| immediatetrans | Checks for inconsistent immediate object address(```&``` operator) usage       |
| mustfree       | Checks for memory leaks (allocate without free)                                |
| usereleased    | Checks if data been use after free                                             |

### stackref
Local static variables are stored in a call stack, when the function's life cycle ends, the call frame is deallocated and all local data of that function are destroyed. ```stackerf``` checks if any pointer points to any of this destroyed data.

For example:

int *glob;
/*@dependent@*/ int *f (int **x){
int sa[2] = { 0, 1 };
int loc = 3;
glob = &loc;
*x = &sa[0];
return &loc;
}

### compdef
Gives warning if function returns a pointer to data which is not completely defined.

For example:

int *f(/*@out@*/ int *x){
	return x;
}

### immediatetrans
Gives warning if inconsistent immediate object address(```&``` operator) exist.

static int tem;

int *f(int *x){

x = &tem;

return x;
}

Since there is no annotation for ```*f```, the return value is assumed to be ```/*@ only @*/```. which means system lost the only pointer points to tem after ```*f``` return.

### mustfree
Provide memory leaks information.

void leak(){

int *ptr = malloc(sizeof(int));

if(ptr != NULL){
*ptr = 1;
}

//free(ptr);

return;
}

Allocate memory without free before return.

### usereleased
Check if system try to use memory which is freed already.

void leak(){

int *ptr = malloc(sizeof(int));

free(ptr);

if(ptr != NULL){
*ptr = 1;
}

return;
}

Use ```*ptr``` after free.

---
## test

#include <stdlib.h>
#define ALLOC(n) (int *) malloc(n)

int main(){
int *p = ALLOC(4);
free(p);
int *t = malloc(3);
free(t);
return 0;
}

return

Splint 3.1.2 --- 03 May 2009

macroMalloc.c:5:17: Parse Error. (For help on parse errors, see splint -help
parseerrors.)
*** Cannot continue.

---
## 16.4 Buffer Overflows

TODO: Why is this unreliable?

| Flag              | Effect                                                            |
| ----------------- | ----------------------------------------------------------------- |
| bounds            | Set both boundsread and boundswrite                               |
| boundsread        | Warning if attempt to read out of boundary, this is not reliable  |
| boundswrite       | Warning if attempt to wrtie out of boundary, this is not reliable |
| likelybounds      | Set both likelyboundsread and boundswrite                         |
| likelyboundsread  | Less powerful than boundsread, but less false warnings            |
| likelyboundswrite | Less powerful than boundswrite, but less false warnings           |

### boundswrite

#### False negative

void f(){

int buf[10];

buf[-1] = 0;

}

Cannot detect ```buf[-1]``` is out of range.
Probably because splint have ```maxset()``` and ```maxread()``` only, without ```minset()``` and ```minread()```.

#### False positive

void f(){

int *buf;

buf = malloc(sizeof(int)*5);
if(buf == NULL){
return;
}

memset(buf,0,sizeof(int)*4);

free(buf);

return;

}

False positive on memset.

#### True positive

void f(){
	
	int buf[10];
	
	buf[10] = 0;

}

Catch ```buf[10]``` is out of range.

---
## 16.5 Function Interface Annotations

---
## 16.6 Summary

---

## Reference list

[1] Testing Static Analysis Tools UsingExploitable Buffer Overflows From Open Source Code [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.87.3364&rep=rep1&type=pdf]

[2] Splint the C code static checker(ppt) [https://www.slideshare.net/UlissesCosta/splint-the-c-code-static-checker]

[3] Splint github [https://github.com/splintchecker/splint]

[4] Static program analysis wikipedia [https://en.wikipedia.org/wiki/Static_program_analysis]

[5] Evans, D., & Larochelle, D. (2002). Improving security using extensible lightweight static analysis. IEEE Software, 19(1), 42–51. doi: 10.1109/52.976940

[6] Splint Publications [https://splint.org/pubs.html]
[7] Splint Bugs [https://splint.org/bugs.html]
[8] Evans, D. (1996). Static detection of dynamic memory errors. Proceedings of the ACM SIGPLAN 1996 Conference on Programming Language Design and Implementation - PLDI 96. doi: 10.1145/231379.231389