search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
173 stars 73 forks source link

Add support for the detection of `CWE-562` #1243

Open mrstanb opened 11 months ago

mrstanb commented 11 months ago

CWE-562 is concerned with the issue of returning an address of a stack variable.

Here's a minimal example of a program that has a CWE-562 weakness:

char *cwe562() {
  char *str;
  return str;
}

I'm not sure if there are any SV-COMP Memory Safety cases for this CWE number (most likely not, at least from what I recall). Nonetheless, I think it'd be useful to have a detection mechanism in Goblint for this type of weakness. In addition, it could potentially be even brought into SV-COMP's Memory Safety category if it'd make sense.

I'll make sure to open a separate PR for this soon.

sim642 commented 11 months ago

In terms of SV-COMP, I think the act of returning such address wouldn't be considered a violation, but if it is then dereferenced, it would be an invalid dereference.

mrstanb commented 11 months ago

In terms of SV-COMP, I think the act of returning such address wouldn't be considered a violation, but if it is then dereferenced, it would be an invalid dereference.

Yes, absolutely. I think in relation to this, we could try to flag such returned memory in some way, so that whenever it's used we could directly flag the use as an invalid one. (Although, thinking about it, we might not need an extra flag, because we could just check if the memory has an address that is not pointing to something local or global and be done with it)

mrstanb commented 10 months ago

Yes, absolutely. I think in relation to this, we could try to flag such returned memory in some way, so that whenever it's used we could directly flag the use as an invalid one. (Although, thinking about it, we might not need an extra flag, because we could just check if the memory has an address that is not pointing to something local or global and be done with it)

We already have a check for such invalid dereferences which was implemented back during my thesis. So even in terms of SV-COMP, we should be safe here.

jerhard commented 2 months ago

Following a dicussion at Gobcon, I closed the PR #1256. We might look again at implementing this when having a look at the escaping of variables, for this see https://github.com/goblint/analyzer/issues/1544, https://github.com/goblint/analyzer/issues/1491.