Skip to content

AdaCore/Http_Cyclone

Repository files navigation

TCP/IP Stack

The project demonstrates how existing software libraries written in C programming language can be hardened in terms of software assurance and security by the use of the Ada and SPARK technologies.

The Oryx Embedded CycloneTCP library is used as a starting point. CycloneTCP is a professional-grade embedded Transmission Control Protocol/Internet Protocol (TCP/IP) library developed by the Oryx Embedded company. The implementation is meant to conform with the Request for Comments (RFC) Internet standards, namely the RFC 793 TCP protocol specifications, provided by the Internet Engineering Task Force (IETF). The library is written in ANSI C, and it supports a large number of 32-bit embedded processors and a large number of Real-time Operating systems (RTOS). It can also run in a bare-metal environment. The library offers implementations for a wide range of TCP/IP protocols. A quick overview of the library can be found here.

A new implementation of the library's socket interface and a partial implementation of the TCP user functions is provided in SPARK. The absence of run-time errors for the translated functions and the conformance to some functional specifications of the TCP norm is proved using the SPARK technologies.

Repository Organization

All the source files need for the compilation are located under the folder src/. In particular, this folder contains the C source files of the CycloneTCP library under the folder cyclone_tcp/. The translated to Ada/SPARK files are located under the subdirectory ada/. The demo's main function is located in the main.c file. The example can compile for the STM32F769I-Discovery, currently supported, development board.

The KLEE symbolic execution engine was used to gain confidence that the C code conforms with the protocol's functional specifications. The folder named klee/ includes all the source files needed to run Klee. A makefile is provided to help with the compilation. The line #include "dns/dns_client.h" in the file net.h might needed to be commented-out to be able to compile. By using the SPARK technologies, the code configured by the prove.gpr file will be proved.

The table below gives an overview of the files that are translated in SPARK and then proved. It also records all the files that offer the necessary bindings between C and Ada to facilitate the interface between the two languages.

File Description Translation or binding
ada_main.adb Customer SPARK code using the socket API. SPARK code.
socket_types.ads Types and structure of a socket. SPARK code
socket_interface.adb Socket API. SPARK code.
socket_helper.ads Helper function for proofs. Helper functions for proofs.
tcp_type.ads Types used for TCP. SPARK code.
tcp_interface.adb TCP user functions. SPARK code.
tcp_misc_binding.adb Helper functions for TCP. SPARK code / binding to C code.
tcp_fsm_binding.ads TCP finite state machine. Functions to process incoming segments. Binding to C code.
tcp_timer_interface.ads Simulate a timer tick. SPARK code. Helper functions for proofs.
udp_binding.adb UDP functions. Binding to C code.
net_mem_interface.adb Memory management. Binding to C code.
ip_binding.adb Underlaying IP layer functions. Binding to C code.

Get the project

Use git clone --recursive <git_repo> to collect all the source files needed.

Dependencies

The following tools are needed to compile the project:

  • GNAT ARM 2020 (download it here https://www.adacore.com/download and install it in the recommended location).
  • OpenOCD to flash on the card (tested with version 2.7.1).
  • [Optional] minicom to see the debug messages (tested with version 0.10.0).

[Optional] For the verification:

  • KLEE + LLVM 6
  • SPARK Pro 22.0w (20201110)

Configuration

The TCP-built configuration options can be set in the file config.def, in the format:

OPTION := VALUE

A description of all the available options can be found in the file options.md.

The TCP-prove configuration options can be set in the file prove.gpr, in the format:

"-gnateDOPTION=VALUE"

If you would like to build and prove for the same configurations, you have to keep the specified options in the config.def and prove.gpr files the same.

Before compiling or running gnatprove, it is necessary to run:

make config

to add the correct files to the compilation.

Compilation

The arm Ada compiler needs to be installed for compiling the project. This can be found here. Please install it at the recommended location.

If the ARM compiler is not installed in the default directory, you can use make RTS=<install_dir> to help the compiler to find the require files for the compilation.

The current implementation supports one development board, namely, the STM32F769I-Discovery.

To compile the project execute:

make

To flash the program onto the STM32 board:

make flash

To view debug messages on the host PC, use:

minicom -D /dev/ttyACM0

Proof

To prove the SPARK code, use:

make prove

or use the following command line:

gnatprove -P prove.gpr --level=4 -j0

The code configured by the config.def will be proved.

Demo

The demo downloads an HTTP page and prints it. To view the printing, you must install and use the minicom tool. To launch the demo, press the blue button on the development board. The page will be displayed as an HTTP request: the header followed by the content of the page in JSON format will be printed.

About

No description, website, or topics provided.

Resources

License

Code of conduct

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •