Commit b7474140 authored by Frédéric Recoules's avatar Frédéric Recoules
Browse files

Release BINSEC 0.4.1

parent 246c388f
## 0.4.1 (2021-12-20)
** Features
- Reworked Backward Bounded Symbolic Execution
(together with some [documentation](doc/bbsse/))
** Misc
- Support native OCaml
[bitwuzla binding](https://github.com/bitwuzla/ocaml-bitwuzla)
** Bug
- Fix an issue with 64-bit kernel virtual addresses
## 0.4.0 (2021-10-12)
** Features
......
# Installing BINSEC from sources
The latest public revision of `binsec` is available on GitHub:
https://github.com/binsec/binsec.
The latest public revision of `unisim_archisec` is available on GitHub:
https://github.com/binsec/unisim_archisec.
A convenient way to build `unisim_archisec` together with `binsec` is to
put `unisim_archisec` directory inside the `binsec` directory.
```console
$ git clone https://github.com/binsec/binsec.git
$ cd binsec
$ git clone https://github.com/binsec/unisim_archisec.git
```
https://github.com/binsec/binsec.
#### Dependencies
Dependencies can be automatically installed via
[*opam*](https://opam.ocaml.org/doc/Install.html).
```bash
$ opam depext -i zarith
$ opam install dune menhir ocamlgraph
$ opam install bitwuzla # optional -- for native SMT solver binding
$ opam install unisim_archisec # optional -- for x86-64, ARMv7 and ARMv8
```
##### System
- [GMP v6.1 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
......@@ -27,6 +26,7 @@ $ git clone https://github.com/binsec/unisim_archisec.git
- [ocamlgraph >= 1.8.5](https://github.com/backtracking/ocamlgraph)
- [zarith >= 1.4](https://github.com/ocaml/Zarith)
- *[unisim_archisec](https://github.com/binsec/unisim_archisec) (optional)*
- *[bitwuzla](https://github.com/bitwuzla/ocaml-bitwuzla) (optional)*
- [odoc](https://github.com/ocaml/odoc) (*documentation*)
- [qcheck](https://github.com/c-cube/qcheck) (*test*)
- [ounit2](https://github.com/gildor478/ounit) (*test*)
......@@ -42,7 +42,7 @@ When `opam` is available, using the command `make` will automatically install th
:information_source: **Local opam switch**
If `opam` is available, using the following command will create a new OCaml switch inside the BINSEC tree.
```bash
OCAML_COMPILER=4.08.0 make switch
OCAML_COMPILER=4.08.1 make switch
```
A local switch makes the installation of dependencies, including ocaml supported version, not impacting the system wide ocaml configuration.
*Doing so, everything installed will be readily available but only inside the BINSEC directory.*
......@@ -60,16 +60,7 @@ make install
#### With `dune`
Make sure the above dependencies are available.
Dependencies can still be automatically installed via
[*opam*](https://opam.ocaml.org/doc/Install.html).
```bash
opam pin add -n . # read the package definition
opam depext binsec # install system dependencies
opam install --deps-only binsec # install OCaml dependencies
opam install --deps-only --with-doc binsec # optional, for documentation
opam install --deps-only --with-test binsec # optional, for tests
```
Make sure the above dependencies are available.
Run the following in order to build `binsec` executable:
```bash
......
......@@ -32,7 +32,7 @@ OCAML_COMPILER ?= $(shell opam switch list | grep -m 1 -oe "ocaml-system[^ ]*")
_opam:
opam switch create . $(OCAML_COMPILER) --no-install
opam install tuareg merlin ocp-indent user-setup -y
opam install tuareg merlin ocamlformat user-setup -y
opam user-setup install
opam pin add . -n
opam install binsec --deps-only --with-test --with-doc -y
......@@ -60,10 +60,19 @@ endef
endif
ifneq (, $(shell which ocamlformat 2> /dev/null))
define apply_ocamlformat
$(shell dune build @fmt --auto-promote)
endef
endif
.PHONY: default switch install uninstall binsec test doc clean
binsec:
$(call check_dune)
$(call apply_ocamlformat)
$(call install_deps,@install)
dune build @install
......
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
version: "0.4.0"
version: "0.4.1"
synopsis: "Semantic analysis of binary executables"
description: """
......@@ -62,7 +62,11 @@ depends: [
"qcheck" {with-test & >= "0.7"}
"odoc" {with-doc}
]
depopts: ["unisim_archisec"]
depopts: [
"llvm" {>= "6.0.0" & < "13.0.0"}
"unisim_archisec"
"bitwuzla" {>= "1.0.1"}
]
build: [
["dune" "subst"] {dev}
[
......
# Commands
## Utils
- File Description
- Disasembly
- Opcode disassembly
## Analysis
- [Static Symbolic Execution](sse)
- [Backward Bounded Static Symbolic Execution](bbsse)
# Backward Bounded Static Symbolic Execution
## Tutorials
- [Tutorial 1: Automatically find opaque predicates](beginners.md)
# BBSSE Tutorial 1: Automatically find opaque predicates
In this post, we will analyze the small binary named
[**echo**](../../examples/bbsse/echo) in search of opaque predicates.
What are we looking for? In order to make reverse-engineering harder, people
may introduce fake conditional jumps. We are especially looking for
jumps with a test that is always true or always false at runtime.
These jumps can be manually inserted, but also automatically added
with obfuscator tools like
[**ollvm**](https://github.com/obfuscator-llvm/obfuscator) or
[**tigress**](https://tigress.wtf/introduction.html).
To find them out, we will exercise the
**B**ackward **B**ounded **S**tatic **S**ymbolic **E**xecution.
**BBSSE** in a nutshell? It tries to answer positively to *infeasible queries*
for all paths of a bounded depth that may reach a given predicate.
You may find interesting to watch our corresponding
[presentation](https://www.youtube.com/watch?v=UU4t0Zvoh-Q) and read our
[S&P 2017 paper](https://binsec.github.io/assets/publications/papers/2017-sp.pdf).
### Requirements
To run to completion we will need:
- a **Linux** environment, preferably on a **x86** machine;
- the **BINSEC** tool (see [install instructions](../../INSTALL.md));
- a SMT solver, preferably [**ocaml-bitwuzla**](../../INSTALL.md#Dependencies)
(but would work with **bitwuzla**, **boolector**, **Z3**, etc.).
The **Ghidra** software revers engineering suite will be required to run
the **BBSSE** on other binaries.
### Getting the Control Flow Graph
First thing out, the backward symbolic engine relies on a precomputed
control flow graph of the program under analysis. **BINSEC** uses the
**Ghidra** tool to obtain the initial graph.
![](../../examples/bbsse/ghidra.svg)
For the need of this tutorial, we already saved the **Ghidra** output in
[ghidra.log](../../examples/bbsse/ghidra.log) but here is the command to generate it on demand.
```console
$ binsec -ghidra -ghidra-analyzeHeadless ${GHIDRA_ROOT}/support/analyzeHeadless -ghidra-cache ghidra.log echo
```
Here, `GHIDRA_ROOT` should be set according to installation path of your
**Ghidra**.
### First invocation
Now we have all what we need, we can run **BINSEC** BBSSE with default option.
```console
$ binsec -ghidra-cache ghidra.log -bbsse-process-all-jumps echo
[bbsse:result] 1 / 9: Predicate jz 0x80480a0 at 08048059 deemed clear
[bbsse:result] 2 / 9: Predicate jnz 0x8048081 at 08048074 deemed opaque branch
[bbsse:result] 3 / 9: Predicate jb 0x8048076 at 0804807b deemed opaque fallthrough
[bbsse:result] 4 / 9: Predicate jnz 0x8048083 at 08048083 deemed clear
[bbsse:result] 5 / 9: Predicate jns 0x80480d9 at 0804808c deemed clear
[bbsse:result] 6 / 9: Predicate jz 0x80480be at 0804809b deemed clear
[bbsse:result] 7 / 9: Predicate jnz 0x8048076 at 0804809e deemed clear
[bbsse:result] 8 / 9: Predicate jnz 0x80480d4 at 080480af deemed opaque fallthrough
[bbsse:result] 9 / 9: Predicate jns 0x80480be at 080480d9 deemed clear
[bbsse:info] total predicate 9
total opaques predicates 3
total unreachable predicates 0
total clear predicates 6
total unfinished (timeout) 0
total explored paths 9
total satisfiability queries 18
total cumulative time 0.028075s
```
**BINSEC** processes all the conditional jumps it finds in the target
binary, making a backward step of `1` basic block to check if both branches
of the jump (`true` and `false`) can be taken.
Here, it found 3 predicates that appear to be opaque:
- predicate `0804074: jnz 0x8048081` is always true and so, will take the branch to `0x804081`;
- predicate `0804807b: jb 0x8048076` is always false and so, will fallthrough at `0x80487d`;
- predicate `080480af: jnz 0x80480d4` is always false and so, will fallthrough at `0x8048b1`.
Can we find more?
### Increasing the number of backward steps
Backward bounded analysis is best effort. The more backward context it gathers,
the more it can be precise. In fact, opaque predicates do not have to be local.
They may rely on a distant initialization or on inconsistencies with parent
predicates.
This is the purpose of the option `-bbsse-max-basic-blocks` (default to `1`).
By setting a higher bound (e.g. `3`), **BINSEC** will gather more history,
enumerating all the paths that could lead to the predicate and checking for
their feasibility.
```console
$ binsec -ghidra-cache ghidra.log -bbsse-process-all-jumps echo \
-bbsse-max-basic-blocks 3
[bbsse:result] 1 / 9: Predicate jz 0x80480a0 at 08048059 deemed clear
[bbsse:result] 2 / 9: Predicate jnz 0x8048081 at 08048074 deemed opaque branch
[bbsse:result] 3 / 9: Predicate jb 0x8048076 at 0804807b deemed opaque fallthrough
[bbsse:result] 4 / 9: Predicate jnz 0x8048083 at 08048083 deemed clear
[bbsse:result] 5 / 9: Predicate jns 0x80480d9 at 0804808c deemed clear
[bbsse:result] 6 / 9: Predicate jz 0x80480be at 0804809b deemed opaque branch
[bbsse:result] 7 / 9: Predicate jnz 0x8048076 at 0804809e deemed clear
[bbsse:result] 8 / 9: Predicate jnz 0x80480d4 at 080480af deemed opaque fallthrough
[bbsse:result] 9 / 9: Predicate jns 0x80480be at 080480d9 deemed opaque branch
[bbsse:info] total predicate 9
total opaques predicates 5
total unreachable predicates 0
total clear predicates 4
total unfinished (timeout) 0
total explored paths 19
total satisfiability queries 28
total cumulative time 0.041755s
```
Here, **BINSEC** found 2 additional opaque predicates.
So, the more, the better? Why not run it with absurdly high value?
Precision comes at a cost. Each additionnal backward step can increase the
number of paths to reason about in an exponential fashion -- especially
with loops.
Empirical experiments tend to show that `3` steps offer the best
trade-off between precision and time.
So, is it all we can do?
### Handling function calls
By default, the backward engine will skip the function calls, replacing them by
a stubs that clobber default caller-saved register (e.g. `eax`, `ecx` and
`edx` for `x86`). This helps scalability, but may introduce false negatives
or, in some corner cases, false positives.
Indeed, it may be necessary to
enter inside the function body to figure out that a predicate is opaque.
This is for instance the case for predicate 5 (`0x804808c`)
which depends on the `ecx` value that is set by the function call at
`0x8048085`.
Let us query the function to be analyzed using `-bbsse-calls-to-proceed`.
```console
$ binsec -ghidra-cache ghidra.log -bbsse-process-all-jumps echo \
-bbsse-max-basic-blocks 3 -bbsse-calls-to-proceed 0x8048085
[bbsse:result] 1 / 9: Predicate jz 0x80480a0 at 08048059 deemed clear
[bbsse:result] 2 / 9: Predicate jnz 0x8048081 at 08048074 deemed opaque branch
[bbsse:result] 3 / 9: Predicate jb 0x8048076 at 0804807b deemed opaque fallthrough
[bbsse:result] 4 / 9: Predicate jnz 0x8048083 at 08048083 deemed clear
[bbsse:result] 5 / 9: Predicate jns 0x80480d9 at 0804808c deemed opaque fallthrough
[bbsse:result] 6 / 9: Predicate jz 0x80480be at 0804809b deemed opaque branch
[bbsse:result] 7 / 9: Predicate jnz 0x8048076 at 0804809e deemed clear
[bbsse:result] 8 / 9: Predicate jnz 0x80480d4 at 080480af deemed opaque fallthrough
[bbsse:result] 9 / 9: Predicate jns 0x80480be at 080480d9 deemed unreachable
[bbsse:info] total predicate 9
total opaques predicates 5
total unreachable predicates 1
total clear predicates 3
total unfinished (timeout) 0
total explored paths 19
total satisfiability queries 27
total cumulative time 0.041881s
```
Here, we found an unreachable predicate because the only way to reach it
is by following the dead branch of an opaque predicate.
Talking about corner cases, there is actually one example in this binary.
The function call at `0x8048094` clobbers the callee saved register `ebx`
without restoring it before returning. Due to the default stub mechanism,
**BINSEC** is reasoning on the wrong value of `ebx` that lead to
a misclassification. We can avoid this by adding the call site to the calls
to proceed.
```console
$ binsec -ghidra-cache ghidra.log -bbsse-process-all-jumps echo \
-bbsse-max-basic-blocks 3 \
-bbsse-calls-to-proceed 0x8048085,0x8048094
[bbsse:result] 1 / 9: Predicate jz 0x80480a0 at 08048059 deemed clear
[bbsse:result] 2 / 9: Predicate jnz 0x8048081 at 08048074 deemed opaque branch
[bbsse:result] 3 / 9: Predicate jb 0x8048076 at 0804807b deemed opaque fallthrough
[bbsse:result] 4 / 9: Predicate jnz 0x8048083 at 08048083 deemed clear
[bbsse:result] 5 / 9: Predicate jns 0x80480d9 at 0804808c deemed opaque fallthrough
[bbsse:result] 6 / 9: Predicate jz 0x80480be at 0804809b deemed clear
[bbsse:result] 7 / 9: Predicate jnz 0x8048076 at 0804809e deemed clear
[bbsse:result] 8 / 9: Predicate jnz 0x80480d4 at 080480af deemed opaque fallthrough
[bbsse:result] 9 / 9: Predicate jns 0x80480be at 080480d9 deemed unreachable
[bbsse:info] total predicate 9
total opaques predicates 4
total unreachable predicates 1
total clear predicates 4
total unfinished (timeout) 0
total explored paths 18
total satisfiability queries 26
total cumulative time 0.043094s
```
This is the best we can do for now analyzing
[**echo**](../../examples/bbsse/echo).
### Discussion
Current version of BBSSE is a complete rework of our original BBSSE.
Code is smaller, simpler and benefits of recent improvements of the **BINSEC**
platform.
We are also experimenting some *incremental* analyses. It is actually possible
to pass multiple (coma separated) values to the option `-bbsse-max-basic-blocks`.
The backward engine then tries to prove the predicates are opaque for the smaller
bounds first, and continues with higher bounds only for the non opaque ones.
It could be very beneficial when you expect to have a lot of *very local*
opaque predicates.
All this brings together, the malware analysis from the S&P 2017 paper runs now
in less than 30 min instead of 1h30 in the original paper (7472 OP detected for
backward depth = `3`), in less than 3 min if we restrict backward depth to 1
(7208 OP detected) and in less than 15 min for incremental mode
(7510 OP detected for backward depth = `1,3`).
Still, loops and function handling are waiting for improvement.
The former prevents the backward engine to find opaque predicates.
The latter may introduce both false negatives and false positives
(especially when functions have a side effect in memory).
Note also that backward engine assumes the precomputed graph is complete.
When it is not the case, false positives may arise.
If interested by these limitations, have a look at the
[S&P 2017 paper](https://binsec.github.io/assets/publications/papers/2017-sp.pdf).
### Conclusion
Congratulation, you successfully learned how to run **BINSEC** backward
symbolic engine to find opaque predicates.
If you are looking for further details about *why the predicates are opaque* and
are not afraid of some reverse-engineering, the
[oracle](../../examples/bbsse/oracle.txt) file compiles the solution of
all `echo` predicates.
Have a nice day :-)
# Tutorial 1: First steps with BINSEC SSE
# SSE Tutorial 1: First steps with BINSEC SSE
In this post, we will exercise the **S**tatic **S**ymbolic **E**xecution engine of **BINSEC** over the small binary puzzle named [**magic**](../../examples/sse/quickstart/magic).
In this post, we will exercise the **S**tatic **S**ymbolic **E**xecution engine of **BINSEC** over the small *CTF* puzzle named [**magic**](../../examples/sse/quickstart/magic).
What are we looking for? *Capture The Flag* games can take the form of a reverse-engineering challenges to find an input (password, etc.) that will reach a special state of the program such as leading to an exploit, a crash or simply printing a victory message.
### Requirements
......
# Tutorial 2: Solving simple CTF with BINSEC SSE
# SSE Tutorial 2: Solving simple CTF with BINSEC SSE
In this post, we will exercise the **S**tatic **S**ymbolic **E**xecution engine of **BINSEC** over the first 2015 [FLARE On](https://flare-on.com/) challenge.
We will do so with the additionnal difficulty of not looking at a single line of code disassembly -- we still reserve the right to use good tools to extract meta-data. This way, we will have to focus on the interaction between the program and its environment (for instance, a user typing in a console) in a *quasi*-black box manner.
......@@ -102,7 +102,7 @@ $ r2 i_am_happy_you_are_to_playing_the_flareon_challenge.exe
```
Here we are fixed, this program is calling the standard C functions [`GetStdHandle`](https://docs.microsoft.com/en-us/windows/console/getstdhandle), [`WriteFile`](https://docs.microsoft.com/en-us/windows/win32/api/fileapi/nf-fileapi-writefile) and [`ReadFile`](https://docs.microsoft.com/en-us/windows/win32/api/fileapi/nf-fileapi-readfile).
It is just an educated guess, but genuin usage scenario suggests:
It is just an educated guess, but genuine usage scenario suggests:
- `WriteFile` arguments:
- `hFile` is the console returned by `GetStdHandle(STD_OUTPUT_HANDLE)`;
- `lpBuffer` points to one of the string `Let's start out easy`, `Enter the password>`, `You are success` or `You are failure`;
......@@ -119,7 +119,7 @@ It is just an educated guess, but genuin usage scenario suggests:
We have some idea of what these functions are supposed to do.
Yet we still ignore at which place they are called.
In fact, for **PE** binaries, the dynamic functions are handled with an `Inport Address Table` that contains the place where
In fact, for **PE** binaries, the dynamic functions are handled with an `Import Address Table` that contains the place where
the dynamic loader has put the functions at runtime. The tool `readpe` can help us to figure out how to mimic this behavior.
```console
$ readpe -di i_am_happy_you_are_to_playing_the_flareon_challenge.exe
......
......@@ -4,7 +4,7 @@
(generate_opam_files true)
(name binsec)
(version "0.4.0")
(version "0.4.1")
(maintainers "BINSEC <binsec@saxifrage.saclay.cea.fr>")
(authors
"Adel Djoudi"
......@@ -55,7 +55,9 @@ An overview of some BINSEC features can be found in our SSPREW'17 tutorial.")
(ounit2 (and :with-test (>= 2)))
(qcheck (and :with-test (>= 0.7))))
(depopts
unisim_archisec)
(llvm (and (>= 6.0.0) (< 13.0.0)))
unisim_archisec
(bitwuzla (>= 1.0.1)))
(tags
("binary code analysis"
"symbolic execution"
......
[kernel]
file = echo
[ghidra]
cache = ghidra.log
[bbsse]
enabled = true
process-all-jumps = true
max-basic-blocks = 3
directives = oracle.txt
This diff is collapsed.
This diff is collapsed.
##########################################################################
# #
# Predicate 1 / 9 #
# #
# 8048055: 8b 34 24 mov (%esp),%esi #
# 8048058: 4e dec %esi #
# 8048059: 74 45 je 0x80480a0 #
# #
# legitimately test if argc is equal to 1. #
# #
##########################################################################
expect 0x8048059 is clear
##########################################################################
# #
# Predicate 2 / 9 #
# #
# 8048061: 8d 44 24 fc lea -0x4(%esp),%eax #
# 8048065: f7 e0 mul %eax #
# 8048067: 8d 5c c0 ff lea -0x1(%eax,%eax,8),%ebx #
# 804806b: 29 c3 sub %eax,%ebx #
# 804806d: 0f b6 07 movzbl (%edi),%eax #
# 8048070: f7 e0 mul %eax #
# 8048072: 39 c3 cmp %eax,%ebx #
# 8048074: 75 0b jne 0x8048081 #
# #
# let x = %esp - 4 and y = (%edi) #
# the equation 8x² - 1 = y² is mathematically impossible. #
# #
##########################################################################
expect 0x8048074 is opaque branch
##########################################################################
# #
# Predicate 3 / 9 #
# #
# 8048079: 85 ed test %ebp,%ebp #
# 804807b: 72 f9 jb 0x8048076 #
# #
# the instruction 'test' always clear the carry flag. #
# #
##########################################################################
expect 0x804807b is opaque fallthrough
##########################################################################
# #
# Predicate 4 / 9 #
# #
# 8048081: 31 c0 xor %eax,%eax #
# 8048083: 75 fe jne 0x8048083 #
# #
# the zero flag is always set. #
# #
##########################################################################
expect 0x8048083 is opaque fallthrough
##########################################################################
# #
# Predicate 5 / 9 #
# #
# 8048085: e8 4a 00 00 00 call 0x80480d4 #
# 804808a: 85 c9 test %ecx,%ecx #
# 804808c: 79 4b jns 0x80480d9 #
# #
# the function at 0x80480d4 always returns -1 in %ecx. #
# require to process call at 0x80480d4 to avoid misclassification. #
# #
##########################################################################
process call at 0x8048085
expect 0x804808c is opaque fallthrough
##########################################################################
# #
# Predicate 6 / 9 #
# #
# 8048092: 31 db xor %ebx,%ebx #
# 8048094: e8 2c 00 00 00 call 0x80480c5 #
# 8048099: 85 db test %ebx,%ebx #
# 804809b: 74 21 je 0x80480be #
# #
# %ebx is part of the callee saved registers. #
# however, the function at 0x80480c5 sets %ebx to 1. #
# require to process call at 0x80480c5 to avoid a false positive. #
# lead to a false negative because of 'int' unsupported instruction. #
# #
##########################################################################
process call at 0x8048094
expect 0x804809b is opaque fallthrough
##########################################################################
# #
# Predicate 7 / 9 #
# #
# 804809d: 4e dec %esi #
# 804809e: 75 d6 jne 0x8048076 #
# #
# legitimately test if all argv has been proceeded. #
# #
##########################################################################
expect 0x804809e is clear
##########################################################################
# #
# Predicate 8 / 9 #
# #
# 80480a4: 31 db xor %ebx,%ebx #
# 80480a6: 43 inc %ebx #
# 80480a7: 8d 44 7f ff lea -0x1(%edi,%edi,2),%eax #
# 80480ab: f7 e7 mul %edi #
# 80480ad: 85 d8 test %ebx,%eax #
# 80480af: 75 23 jne 0x80480d4 #
# #
# let x = %edi #
# the expression (3x - 1) * x can not be odd. #
# #
##########################################################################
expect 0x80480af is opaque fallthrough
##########################################################################
# #
# Predicate 9 / 9 #
# #
# its predecessor at 0x0804808c can not jump to it. #
# #
##########################################################################
expect 0x80480d9 is unreachable
......@@ -5,6 +5,3 @@ file = IgniteMe.exe
enabled = true
depth = 100000
script = crackme.ini
[fml]
solver = bitwuzla
......@@ -5,6 +5,3 @@ file = unbreakable-enterprise-product-activation
enabled = true
load-sections = .rodata,.data,.bss
script = crackme.ini,strncpy.stub,exit.stub
[fml]
solver = bitwuzla
\ No newline at end of file
(**************************************************************************)
(* This file is part of BINSEC. *)
(* *)
(* Copyright (C) 2016-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)