Code one C Manual de usuario descargar pdf (Pagina 12)

• mops ld: a linker that takes a set of CFG ﬁles and

merges them into a single CFG ﬁle, resolving cross

references of external functions and variables.

• mops

check: the model checker that takes a CFG and

an FSA and decides if the program may violate the

security property in the FSA.

Our build integration mechanism is built on top of these

three core components. Amusingly, it took us three major

iterations before we settled upon an acceptable method for

integrating MOPS into the applications’ build processes.

First try: running MOPS by hand In our ﬁrst imple-

mentation, we provided no build integration support at all:

the user was forced to run the above three programs by

hand. This quickly proved unwieldy for packages contain-

ing multiple source ﬁles and also made it tricky to ensure

that mops

cc received the same options as the real cc.

Second try: modifying Makeﬁle The next thing we

tried was to integrate these three programs into the build

process of the package manually. As a ﬁrst attempt, we

tried to put these programs into the Makeﬁle of each pack-

age. Although this works on packages with simple Make-

ﬁles (e.g., OpenSSH), it quickly becomes unusable on

packages with complicated and multiple Makeﬁles. Fur-

thermore, rerunning autoconf will remove any modiﬁca-

tions to Makeﬁles. Therefore, we soon discovered that we

needed an automatic approach for integrating MOPS into

the build process.

Third try: interposing on GCC Our solution was to

hook into GCC. Most packages use GCC to build executa-

bles. By setting the GCC

EXEC PREFIX environment

variable, we instruct the GCC front-end to use mops

cc as

the parser instead of cc1 and mops

ld as the linker instead

of collect2. So after we build the package, each object ﬁle

contains a CFG from a single source program ﬁle and each

executable ﬁle contains a merged CFG instead of machine

code that GCC would normally build. A nice side beneﬁt

of this approach is that we can be sure that MOPS runs

on exactly the (preprocessed) code that is compiled, since

mops

cc runs after the preprocessor (cpp).

Reﬁnement: building both CFGs and machine code

The above process does not build any machine code.

This causes problems in some packages, which build and

run executables to generate header ﬁles needed for future

compilation. Since the above MOPS process replaces ex-

ecutables with CFGs, it causes these packages to fail to

build. Similarly, it breaks autoconf. An obvious solution

is to let mops

cc, for each program ﬁle foo.c, build both

a CFG ﬁle foo.cfg and a machine code ﬁle foo.o. Also

mops

ld should link not only the CFG ﬁles but also the

machine code ﬁles.

Reﬁnement: combining each CFG and its machine

code into one ﬁle The above process, however, causes

yet some other packages to fail because of the weak link-

age between machine code (.o ﬁles) and CFGs (.cfg ﬁles).

In some packages, the build process moves an object ﬁle,

renames it, or puts it into an archive. In such cases, the

corresponding CFG ﬁle is left dangling and the link to

the .o ﬁle is broken. A possible solution is to modify

the PATH environment variable to trap the commands that

cause the above problems, such as mv, ar, etc. This,

however, is laborious and is hard to make complete. In-

stead, we adopted an approach that takes advantage of the

ELF ﬁle format, which allows multiple sections. Since

GCC generates object ﬁles and executables in ELF, we

extended mops

cc and mops ld to insert CFGs into a com-

ment section in the appropriate object ﬁles and executable

ﬁles. Then, mops

check extracts CFGs from executables

for model checking. This way, a CFG is always in the

same ﬁle as its corresponding machine code, no matter

how the build process moves, renames, or archives the ﬁle,

the ﬁdelity of MOPS’s analysis is ensured.

Finally, we wrote a front-end that lets the user run

MOPS on packages distributed as .tar ﬁles or source

RPM packages at the push of a button. The user sim-

ply provides the front-end with the packages and the se-

curity properties, and the front-end will invoke the model

checker on the packages using their appropriate build pro-

cesses. This push-button capability has made a signiﬁcant

qualitative difference in our use of MOPS: by removing

artiﬁcial barriers to use of MOPS, it has freed us up to

spend the majority of our time on the code auditing task

itself. For packages with special build processes, we can

modify their Makeﬁles to use mops

cc as the compiler, use

mops

ld as the linker, and do model checking immediately

after linking. In this way, we have integrated MOPS into

the build process of EROS (Extremely Reliable Operating

System) [19].

5.3. Value of Tool Support

It is striking that we were able to ﬁnd so many bugs

in these mature, widely used software packages that are

probably among the best designed, implemented, audited

packages around. Given that MOPS can ﬁnd security bugs

in these programs, our experience suggests that we proba-

bly cannot have conﬁdence in the rest of our software.

Static analysis tools like MOPS are valuable in ﬁnd-

ing vulnerabilities in the programs that run today, but

they are even more valuable in preventing vulnerabili-

ties from being inadvertently introduced into programs

1 2 ... 7 8 9 10 11 12 13 14 15

Comentarios a estos manuales

Sin comentarios

Code one C Manual de usuario Pagina 12

Comentarios a estos manuales

Relacionado con productos y manuales para Detectores de humo Code one C