fedora 25
misc weakness #442

4

Weakness Breakdown


Definition:

The software specifies permissions for a security-critical resource in a way that allows the resource to be read or modified by unintended actors.

Warning code(s):

Exactly what cuserid.

File Name:

frama-c-Silicon-20161101/share/libc/unistd.h

Context:

The highlighted line of code below is the trigger point of this particular Fedora 25 misc weakness.

 #define __FC_MAX_OPEN_FILES 1024

// __fc_fds represents the state of open file descriptors.
//@ ghost int __fc_fds[__FC_MAX_OPEN_FILES];
// TODO: Model the state of some functions more precisely.
// TODO: define __fc_fds as volatile.


int          access(const char *, int);
unsigned int alarm(unsigned int);
int          brk(void *);
int          chdir(const char *path);
int          chroot(const char *path);
int          chown(const char *, uid_t, gid_t);

/*@
  requires 0 <= fd < __FC_MAX_OPEN_FILES;
  assigns \result, __fc_fds[fd] \from fd, __fc_fds[fd];
  ensures \result == 0 || \result == -1;
*/
int          close(int fd);
size_t       confstr(int, char *, size_t);
char        *crypt(const char *, const char *);
char        *ctermid(char *);
char        *cuserid(char *s);
int          dup(int);
int          dup2(int, int);
void         encrypt(char[64], int);

/*@ requires arg != \null;
    requires valid_read_string(path);
    requires valid_read_string(arg);
    assigns \result \from path[0..], arg[0..];
*/
int          execl(const char *path, const char *arg, ...);
/*@ requires arg != \null;
    requires valid_read_string(path);
    requires valid_read_string(arg);
    assigns \result \from path[0..], arg[0..];
*/
int          execle(const char *path, const char *arg, ...);
/*@ requires arg != \null;
    requires valid_read_string(path);
    requires valid_read_string(arg);
    assigns \result \from path[0..], arg[0..];
*/
int          execlp(const char *path, const char *arg, ...);
/*@ requires argv[0] != \null;
    requires valid_read_string(path);
    requires valid_read_string(argv[0]); 

The registered trademark Linux® is used pursuant to a sublicense from the Linux Foundation, the exclusive licensee of Linus Torvalds, owner of the mark on a world­wide basis.