4. The Story about Codex Assumptions (Mini-OS?)

This page documents all the assumptions Codex currently makes with regards to properties of the ELF Application containg an Operating System and its Tasks to be analyzed. While the stated goal of Codex has been analysis of any operating system, some information can not be automatically inferred, such as the entry point of the kernel.

Two mechanisms are currently used to add information: - Symbols (in the ELF binary) - Annotations (in Codex source code)

Finally certain behaviour is required from some symbols: _start in particular seems expected to prepare the system for task-switching, and eventually drop privileges. An incomplete analysis is presented in section Behaviour of _start.

4.1. Symbols

• _begin_of_all: (address label)

  Indicates start of kernel- and user-code address space, i.e. code and data segments.

• _end_of_readonly: (address label)

  Indicates end of read-only kernel- and user-code address space, i.e. after code, before data. Because Codex does not support self-modifying code, this must be start of, or offset into data segment.

• _end_of_kernel: (address label)

  Despite its name, this appears to indicate the end of both kernel and user application. TBD: validate this assumption!

• user_tasks_image: (address label)

  Start of structured data describing all tasks to the Operating System. OS-specific, structure implemented in Codex at src/codex/x86_types.ml.

• _start: (function)

  Probably the kernel entry point.

• asm_syscall_handler: (function)

• copy_context:

• error_infinite_loop:

• init_reserve:

• fatal:

• terminal_initialize:

• terminal_newline:

• terminal_writestring: These are functions are OS-specific, and have custom handling implemented in Codex at src/codex/x86_settings.ml.

There are more symbols not yet documented, because they are only used in a later execution stage of Codex - such as _start_of_user_tasks. TODO: add them here!

4.2. Annotations

Codex source files src/codex/x86_settings.ml and src/codex/x86_types.ml contains most of the annotations. They allow the abstract interpretation to reason about saved registers, stack pointers and address spaces that are used for context switching - and specify expected invariants that must hold for error-free execution.

4.3. Experiments

4.3.1. Learning about Symbol Lookups

The following one-line change can be added to Codex, so that every time a symbol is looked up - a message appears on stdout for later use:

diff --git a/binsec/src/loader/loader_utils.ml b/binsec/src/loader/loader_utils.ml
index 0110fa8..c519adb 100644
--- a/binsec/src/loader/loader_utils.ml
+++ b/binsec/src/loader/loader_utils.ml
@@ -28,6 +28,7 @@ let get_byte_at img addr =

 let address_of_symbol ~name img =
   let symbols = Loader.Img.symbols img in
+  Printf.printf "Looking for symbol %s\n" name;
   try
     Some (Loader.Symbol.value
             (Array_utils.find

4.3.2. Tracing Exceptions

Binsec has not been designed to print meaningful error messages, when its assumptions on particular features of the input executable do not hold. Error messages can look inconclusive:

[codex:debug] attempt to set esp
[codex:debug] Setting esp to ( + [--..--], Top)
[codex:debug] load: returns Bottom
minor_words:     5275096
major_words:      574656
promoted_words:   484821
total_allocated: 5364931
Fatal error: exception Not_found

As a first hint, OCaml does support showing traces when exceptions occur. This feature can be activated for any OCaml binary with debug info (built with -g, unstripped) through the OCAMLRUNPARAM environment variable:

The extended output for the exception above shows the entire call-trace, indicating which source-files and line numbers lead to the exception:

4.3.3. Minimal 386 assembly

For complete symbol happiness, and to get Codex to startits interpretation, a small program can be written in assembly, without any meaningful application logic - as basis for further experiments. This program does not complete all symbols used by Codex yet, only those discovered during operating-system startup (_start).

	.global _start

	.text
_begin_of_all:

_start:
	// do nothing, then terminate in error state
	nop
	jmp error_infinite_loop

// end execution in infinite loop
fatal:
error_infinite_loop:
	jmp error_infinite_loop

asm_syscall_handler:
copy_context:
init_reserve:
terminal_initialize:
terminal_newline:
terminal_writestring:
	// do nothing, then return
	ret

// code should be read-only (self-modifying not supported by codex)
_end_of_readonly:

	.data

// user-code kernel API (dummy)
user_tasks_image:
	.space 28

// end of kernel-space
_end_of_kernel:

after code

4.4. Behaviour of _start

The first execution stage interprets operating system startup, by following the _start symbol. There is a currently unknown implicit expectation from codex for how start must terminate. When this expectation isn’t met, a rather meaningless error similar to the following will be generated:

minor_words:     4913804
major_words:      561295
promoted_words:   474994
total_allocated: 5000105
Fatal error: exception Not_found

The authors of Codex have provided 4 example combinations of educrtos, user tasks and injected errors. The educrtos example with 10 tasks, also called rq3, is used for a side-by-side comparison with a minimal elf application producing the aforementioned error. During analysis, several dot-files are generated that represent the execution trace traversedby Codex. The first generated trace is init_cpu0.dot. It is the result of analysing the _start symbol - which should implement operating-system startup and initialization of state. When the error condition occurs, this is also the only graph generated - indicating that the problem lies within _start or its analysis.

From the trace above it is clear that analysis eventually terminates at address 0xcafecaf0. Based on comments in the Codex implementation, this is a mock address for internal purposes. The previous execution point is at 0x104125. A disassembly from objdump shows that 0x104125 is near the end of the hw_context_switch_no_idle function, where the DS register is overwritten with an unknown value from memory.

0010407d <hw_context_switch_no_idle>:

  104120:       e8 ef 0c 00 00          call   104e14 <copy64>
  104125:       8e 5b 30                mov    ds,WORD PTR [ebx+0x30]
  104128:       89 dc                   mov    esp,ebx
  10412a:       61                      popa
  10412b:       cf                      iret

Further experiments with explicitly modifying the DS register in custom code did not lead to success. Rather it appears that Codex is waiting for a change in execution privilege level. This is very likely hidden right in the write to DS. Values written to the 386 segment registers include a 5-bit index into either the General Description Table or a Local Description Table, an additional bit to choose between GDT and LDT, and finally 2 bits to specify a permission level. As the value written is not easily known, a different experiment is needed to gain more insight into this suspicion:

The error message can be traced to a particular piece of Codex code near the end of the analyze-function:

(* Do an analysis and returns the set of written data addresses, the set of
 * read data addresses, and the state at {expected_last_instr} (or one of them,
 * if it is present several times in the CFG). If {expected_last_instr} is not
 * in the CFG, {Invalid_argument} is thrown. *)
let analyze img start ctx init_state graph_filename expected_last_instr =
  ...
  if not except_thrown then begin
    ...
    match expected_last_instr with
    | Some instr ->
        let final_state = Regex_tbl.latest_state instr in
        ret, Some final_state, Record_cfg.visited_instructions trace
    | None -> ret, None, Record_cfg.visited_instructions trace
  end

diff --git a/binsec/src/codex/analyze.ml b/binsec/src/codex/analyze.ml
index 012de0c..dbb483b 100644
--- a/binsec/src/codex/analyze.ml
+++ b/binsec/src/codex/analyze.ml
@@ -870,6 +870,7 @@ let analyze img start ctx init_state graph_filename expected_last_instr =
     let ret = !written_data_addrs, !read_data_addrs in
     written_data_addrs := empty; read_data_addrs := empty;
     (* Return state at {expected_last_instr} *)
+    Printf.printf "Going to match Record_cfg.visited_instructions with expected_last_instr %s\n" to_string expected_last_instr;
     match expected_last_instr with
     | Some instr ->
         let final_state = Regex_tbl.latest_state instr in

At this point the abstract interpretation has finished, and something called an expected last instruction is searched in the execution trace, but - according to the error message - “Not_found”. By adding a printf right above the matching logic, this particular moment in Codex execution can be uniquely identified in its length debug output.

First, with the failing application:

$ binsec -config binsec.ini app.exe -codex-x86-types rr -codex-nb-tasks 1 -codex-no-dyn-threads -codex-debug-level 9
...
[codex:debug] Dereferenced type: ParamT ((context)[10]* with (self != 0),
               + {0},  + {-10}, 0)
Going to match Record_cfg.visited_instructions with expected_last_instr
minor_words:     4953047
major_words:      564207
promoted_words:   477486
total_allocated: 5039768
Fatal error: exception Not_found

Then with the known educrtos binary:

[codex:debug] Setting OF to ( + [--..--], Top)
[codex:debug] attempt to set NT
[codex:debug] Setting NT to ( + [--..--], Top)
[codex:debug] attempt to set RF
[codex:debug] Setting RF to ( + [--..--], Top)
[codex:debug] attempt to set AC
[codex:debug] Setting AC to ( + [--..--], Top)
[codex:debug] attempt to set ID
[codex:debug] Setting ID to ( + [--..--], Top)
[codex:debug] attempt to set IF
[codex:debug] Setting IF to ( + [--..--], Top)
[codex:debug] attempt to set IOPL
[codex:debug] Setting IOPL to ( + [--..--], Top)
[codex:debug] attempt to set VIF
[codex:debug] Setting VIF to ( + [--..--], Top)
[codex:debug] attempt to set VIP
[codex:debug] Setting VIP to ( + [--..--], Top)
[codex:debug] attempt to set cpl
[codex:debug] Setting cpl to ( + {-1}, Top)
Going to match Record_cfg.visited_instructions with expected_last_instr

The Full log-file is available here: codex_assumptions/codex-educrtos-debug.log

The last event changes the privilege level, right after what looks like a full context switch. This seems to confirm that Codex expects _start to eventually lead to either context switch, or dropping of privilege. Further effort will be required to confirm what exactly it is, or find a small example.