Path-Aware Static Program Analyses for Specification Mining* - Mining Software Specifications: Methodologies and Applications - page 319

illustrative to demonstrate the technique for a procedure such as bind , which
has a well-documented interface. The bind system call takes three parameters,
viz., a socket descriptor (type: int ), the local address to which the socket
needs to bind (type: structsockaddr* ), and the length of the address
(type: socklent ). For a stream socket to start receiving connections, it needs
to be assigned to an address, which is achieved by using bind . Summarizing
the documentation, the necessary conditions that must hold before bind can
be called are:
(a) A socket system call must have occurred.
(b) The return value of socket must have been checked for validity.
(c) The address (second parameter to bind ) corresponds to a specific ad-
dress family (e.g., AF UNIX, AF INET).
The first condition defines a precedence constraint, while the second and
third define dataflow properties. Ideally, our goal is to obtain the above infor-
mation by tracking various calls to bind in the source. Figure 9.3 shows code
fragments of two procedures (out of eight, total) that invoke the bind system
call in openssh-4.2p1 .
Figure 9.3(a) shows a code fragment from the file sshd.c where bind is
invoked from main . Before the call to bind , as per the documented require-
ments, observe that there is a call to socket on line 1287. The returned value
listensocket is checked to ensure that it is a valid descriptor, and the ad-
dress is set (lines 1075 and 1272). In fact, in a convoluted chain, the procedure
filldefaultserveroptions in main invokes addlistenaddr , which in
turn invokes addonelistenaddr where the address that is eventually used
in bind is set. Apart from these known requirements, other operations de-
pendent on the application context are also performed (e.g., the family of the
address is checked in line 1273, the numlistensocks is checked in line 1275,
etc.). By observing just a single use of bind alone, we can generate some
properties on the required operations before bind is called.
Table 9.1 shows the subset of properties generated for the corresponding
bind call. For example, we observe a property where a variable listensock is
assigned the return value of socket , has a value greater than or equal to 0, and
is the first parameter in calls to setsockopt and bind . As explained earlier,
these properties form some of the preconditions for calls to bind . However,
not all properties generated before this bind call need to hold always before
any other call to bind . For example, ret is assigned the return value of
getnameinfo and is equal to 0 before the bind call. This property may be
relevant in the context of calls to bind in sshd.c , but may not be relevant
in calls made within other files. Unfortunately, simply examining this single
call without any a priori knowledge of bind 's behavior would not permit us
to discard this property from its specification.