Null Byte Array Domain #1076

nathanschmidt · 2023-06-06T14:20:25Z

This PR implements a Null Byte Array Domain tracking all indexes of array elements thay may be null and must be null. Additionally, it also memorizes the size of the array. It is always run as part of the AttributeConfiguredArrayDomain, which allowed an easy extension of the cases for the functions listed above in the base analysis.

This domain makes it possible to gain meaningful information for strings, especially concerning the effects of the functions strcpy, strncpy, strcat, strncat, strlen, strstr, strcmp and strncmp. On top, the domain tries to identify possible and sometimes even certain buffer overflows.

TODOs:

map all array elements that are read-in to null () resp. not_null ()
tackle TODO annotations in code
write test cases for both sound uses of the functions and scenarios for which warnings should be triggered

…nt-analyzer into null-byte-arrayDomain

TODO: strstr, strcmp and strncmp TODO: check and simplify code TODO: update string functions case in base analysis using new domain

…nt-analyzer into null-byte-arrayDomain

src/cdomains/arrayDomain.ml

michael-schwarz · 2023-06-07T15:06:50Z

I'll review the things in base and the NullByteDomain for now, we agreed that the rest needs some changes.

- Updated null recognition in Compound of valueDomain - strstr analysis can now detect NULL ptr - fixed get of AttributeConfiguredArrayDomain

…-byte-arrayDomain

- Null Byte domain can now be called for all wished functions in base and values are correctly updated - Base now sets dest to top if string functions receive an array as dest and a string literal as src - Added function setting whole array content to top but still memorizing type and size - Fixed inverted comparisons in string_copy - Fixed wrong claim in string_comparison

src/common/util/options.schema.json

tests/regression/73-strings/01-string_literals.c

tests/regression/73-strings/03-string_basics.c

sim642 · 2023-11-29T08:53:20Z

src/cdomains/nullByteSet.ml

+module MaySet = struct
+  module M = SetDomain.ToppedSet (IntDomain.BigInt) (struct let topname = "All Null" end)
+  include M


Nothing prevents this set from growing unbounded, does it?

No, there's no such guarantee. There's some attempt to represent sets that comprise the full range by top, but that is not done consistently.
My ambition at some point was to decouple the set nature of this from the analysis to admit other abstractions here (e.g. our int domains). But I did not get around to doing this.

Indeed, we already have interval sets and they're simply a generalization of this, so that should be possible but is probably too much work for now.

sim642 · 2023-11-29T09:03:22Z

src/analyses/base.ml

+            (* if s string literal, compute strlen in string literals domain *)
+            if AD.type_of a = charPtrType then
+              Int (AD.to_string_length a)


Polymorphic comparison of types. But also, I'm not sure how reliable this type-based check is because looks like it's trying to check for StrPtr. But there may be a char* which isn't StrPtr.

src/analyses/base.ml

sim642 · 2023-11-29T09:12:02Z

src/analyses/base.ml

+    let address_from_value (v:value) = match v with
+      | Address a ->
+        let rec lo = function
+          | `Index (i, `NoOffset) -> `NoOffset
+          | `NoOffset -> `NoOffset
+          | `Field (f, o) -> `Field (f, lo o)
+          | `Index (i, o) -> `Index (i, lo o) in
+        let rmLastOffset = function
+          | Addr.Addr (v, o) -> Addr.Addr (v, lo o)
+          | other -> other in
+        AD.map rmLastOffset a
+      | _ -> raise (Failure "String function: not an address")


Why can the last index just be ignored unconditionally. I find it odd because this looks like Offset.remove_offset but that one also consistently removes fields.

Also, this is just called address_from_value and exposed in quite large scope, which is prone to misuse. If the logic is indeed exactly as needed, then this should have a different name or be withint string_manipulation or whereever.

The idea is that the framework has tacked on a [0] offset to string pointer somewhere, but we do want the raw pointer here. You are probably right about naming and moving to a different scope.

May be, but there must be a more reliable way to know when this needs to be dropped. Because this also drops such indices when they explicitly occur in the program, rather than being inserted by CIL, and then we would likely do something wrong. For example, what about an array of strings (i.e. multi-dimensional array of chars).

I have not investigated this in detail, but agree someone should ideally do so.

sim642 · 2023-11-29T09:13:35Z

src/cdomains/valueDomain.ml

  val invalidate_value: VDQ.t -> typ -> t -> t
+  val invalidate_abstract_value: t -> t


Why a different thing here? If we're dealing with strings, surely we know the type, no?

nathanschmidt added 9 commits May 18, 2023 14:47

Merge branch 'base-string-analyses' of github.com:nathanschmidt/gobli…

3ca0419

…nt-analyzer into null-byte-arrayDomain

Very first (incomplete) draft for Must Null Byte Domain

2a53cbb

Draft for complete Null Byte Domain

7798c04

TODO: strstr, strcmp and strncmp TODO: check and simplify code TODO: update string functions case in base analysis using new domain

Added functions for strstr and str(n)cmp to Null Byte Domain

d59b45e

First adaptations to AttributeConfiguredArrayDomain

7a41dc4

Finished draft of Null Byte Array Domain

f940d01

Merge branch 'base-string-analyses' of github.com:nathanschmidt/gobli…

8915ae9

…nt-analyzer into null-byte-arrayDomain

Merge branch 'base-string-analyses' of github.com:nathanschmidt/gobli…

fa3f7f6

…nt-analyzer into null-byte-arrayDomain

Merge branch 'base-string-analyses' of github.com:nathanschmidt/gobli…

9fc814d

…nt-analyzer into null-byte-arrayDomain

github-advanced-security bot found potential problems Jun 6, 2023

View reviewed changes

Addressed github-code-scanning suggestions

a912463

michael-schwarz requested review from michael-schwarz and sim642 and removed request for sim642 June 7, 2023 09:15

nathanschmidt and others added 9 commits June 8, 2023 12:38

Fixed integration of domain for base analysis

fb65c1c

- Updated null recognition in Compound of valueDomain - strstr analysis can now detect NULL ptr - fixed get of AttributeConfiguredArrayDomain

Fixed incompatible ikinds: changed !Cil.kindOfSizeOf to ILong

b49a043

Merge branch 'goblint:master' into null-byte-arrayDomain

6023d47

Introduced case for value = bot in make of NullByte

00941e7

Merge branch 'goblint:master' into null-byte-arrayDomain

85d8ae6

Merge remote-tracking branch 'origin/null-byte-arrayDomain' into null…

e3a03cd

…-byte-arrayDomain

Handle bot for MustNulls / top for MayNulls properly

03085f5

Added new thorough regression test

44bd644

michael-schwarz requested a review from sim642 June 14, 2023 14:56

sim642 added feature student-job precision labels Jun 15, 2023

nathanschmidt and others added 2 commits June 29, 2023 21:03

Feature: better treatment of edge cases

472ece8

Pass argument to move_if_affected

6bf2d77

michael-schwarz added 10 commits November 28, 2023 20:11

Replace exists types with options

55a0dd4

Make types in string_concat make sense

7a2e9ba

Simplify

1282af3

Pull out helper

c85bad9

One less May/MustSet

20ee375

Decouple concrete sets from MaySet

d995cc9

Simplify

72476fb

Lift one more transfer function to work on MustMay

a73c28d

Use option type

c15ca04

Strange parens

1a9ce2c

michael-schwarz marked this pull request as ready for review November 28, 2023 20:58

michael-schwarz and others added 5 commits November 28, 2023 22:06

Merge branch 'master' into null-byte-arrayDomain

672650b

Deduplicate ArrayDomain.StrWithDomain declarations

df60d52

Remove trailing whitespace in ArrayDomain

309f000

Use ocamldoc references in ArrayDomain.Str

44705f4

Deduplicate Null declarations

80c2694

sim642 reviewed Nov 29, 2023

View reviewed changes

sim642 self-requested a review December 5, 2023 13:39

sim642 added 3 commits December 11, 2023 10:50

Fix invalid free in 73-strings/03-string_basics

77b4f67

Add TODOs related to null byte array domain

f2fdb62

Merge branch 'master' into null-byte-arrayDomain

4577879

sim642 added this to the v2.4.0 milestone Dec 12, 2023

sim642 merged commit c90eb12 into goblint:master Dec 12, 2023
9 of 10 checks passed

sim642 added a commit that referenced this pull request Dec 12, 2023

Add NullByteSet to API documentation (PR #1076)

0d299f4

sim642 added a commit that referenced this pull request Dec 12, 2023

Fix NULL byte domain indentation (PR #1076)

6500d35

sim642 mentioned this pull request Jan 25, 2024

Unsoundness from null-byte arrayDomain merge #1337

Open

michael-schwarz mentioned this pull request Mar 10, 2024

Improve output for NullByte domain #1386

Closed

sim642 mentioned this pull request Aug 2, 2024

[new release] goblint (2.4.0) ocaml/opam-repository#26327

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Null Byte Array Domain #1076

Null Byte Array Domain #1076

nathanschmidt commented Jun 6, 2023 •

edited

Loading

michael-schwarz commented Jun 7, 2023

sim642 Nov 29, 2023

michael-schwarz Nov 29, 2023 •

edited

Loading

sim642 Nov 29, 2023

sim642 Nov 29, 2023

sim642 Nov 29, 2023

michael-schwarz Nov 29, 2023

sim642 Nov 29, 2023

michael-schwarz Nov 29, 2023

sim642 Nov 29, 2023

		val invalidate_value: VDQ.t -> typ -> t -> t
		val invalidate_abstract_value: t -> t

Null Byte Array Domain #1076

Null Byte Array Domain #1076

Conversation

nathanschmidt commented Jun 6, 2023 • edited Loading

michael-schwarz commented Jun 7, 2023

Choose a reason for hiding this comment

michael-schwarz Nov 29, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nathanschmidt commented Jun 6, 2023 •

edited

Loading

michael-schwarz Nov 29, 2023 •

edited

Loading