---
# System prepended metadata

title: Security and Dependability Aspects
tags: [NCKU, lesson, splint]

---

# 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:
``` splint -flag +flag code.c```
And annotation is defined in code:
```/*@null@*/ int *p;```

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
```/*@null*/ int num;``` Value of ```num``` could be ```NULL```.
```/*@null*/ int *fun(){}``` return of function ```fun``` could be ```NULL```.

### enum
enum is a datatype, for example:
```cpp=
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:
```cpp=
1
4
3
```


```/*@ -enumint @*/``` Cannot put ```int``` value directly into a ```enum``` datatype, for example:
```cpp=
/*@ -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:
```cpp=
int *glob;
/*@dependent@*/ int *f (int **x){
    int sa[2] = { 0, 1 };
    int loc = 3;
    glob = &loc;
    *x = &sa[0];
    return &loc;
} 
```

```glob``` on line 5 pointed to local address ```&loc```, which will become a invalid address after ```*f``` ends.
```*x``` pointed to local array ```sa```, which is also invalid after ```*f``` ends.

```/*@dependent@*/``` is needed because there is a implicit ```/*@only@*/``` for ```*f```.

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

For example:
```cpp=
int *f(/*@out@*/ int *x){
	return x;
}
```

```/*@out@*/``` annotation tells that ```*x``` might not defined. Clearly ```*f``` returned a value which might not defined.

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

```cpp=
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.

```cpp=
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.

```cpp=
void leak(){
	
	int *ptr = malloc(sizeof(int));
	
	free(ptr);
    
    if(ptr != NULL){
		*ptr = 1;
	}
	
	return;
}
```

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

---
## test

```cpp
#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
```cpp=
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

```cpp=
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.
```bounds.c:10:2: Possible out-of-bounds store: memset(buf, 0, sizeof(int) * 5)```

#### True positive
```cpp=
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
