i#2283: Facilitate Umbra Layouts with Constraint Solving. #2300

johnfxgalea · 2020-06-19T10:08:22Z

Adds a helper python script to facilitate the setting up of Umbra Shadow Memory Layouts. Given the details of a memory layout, such as mask and disp values, the script will check whether any collisions are present with respect to the current pre-defined app regions that Umbra 64-bit considers today.

Example:

python3 umbra_layout.py --os linux --mask 0xFFFFFFFFFFF --disp 0x120000000000
Information:
	OS: linux
SUCCESS

Memory Layout:

	Disp: 0x0000120000000000
	Mask: 0x00000FFFFFFFFFFF
	Unit Size: 0x0000100000000000
	Scale: 0
	Map Count: 1 

MAP 0
	app0:	 [0x0000000000000000, 0x0000010000000000] : exec,heap, data
	shd0:	 [0x0000120000000000, 0x0000130000000000]


	app1:	 [0x0000550000000000, 0x0000570000000000] : pie
	shd1:	 [0x0000170000000000, 0x0000190000000000]


	app2:	 [0x00007F0000000000, 0x0000800000000000] : lib, map, stack, vdso
	shd2:	 [0x0000210000000000, 0x0000220000000000]

The script also uses a constraint solver (namely Z3) to check a layout as well as synthesize satisfying displacement values that result in no collisions (if sat).

Example:

python3 umbra_layout.py --os linux --scale up_2x --mask 0xFFFFFFFFFFF --verify
Information:
	OS: linux
SUCCESS

Memory Layout:

	Disp: 0x0000140000000000
	Mask: 0x00000FFFFFFFFFFF
	Unit Size: 0x0000100000000000
	Scale: 1
	Map Count: 1 

MAP 0
	app0:	 [0x0000000000000000, 0x0000010000000000] : exec,heap, data
	shd0:	 [0x0000280000000000, 0x00002A0000000000]


	app1:	 [0x0000550000000000, 0x0000570000000000] : pie
	shd1:	 [0x0000320000000000, 0x0000360000000000]


	app2:	 [0x00007F0000000000, 0x0000800000000000] : lib, map, stack, vdso
	shd2:	 [0x0000460000000000, 0x0000480000000000]

derekbruening · 2020-06-19T14:01:52Z

I was going to say, don't we already have some of this: but it looks like the app I have is not checked in anywhere. It doesn't have a sat checker (used manual loops in the past). It does, however, check all the scales (up 2x, down 2x, down 4x, down 8x) for any particular setting, if you could add that here. I put it at #2301 (not to commit it just for comparison).

The checked-in test we have is umbra_client_allscales but it only checks the checked-in config.

johnfxgalea · 2020-06-19T18:47:58Z

It does, however, check all the scales (up 2x, down 2x, down 4x, down 8x) for any particular setting.

So the script already allows one to check a layout for a given scale. I can add support to the script to check all scales but I wonder what the benefit is because Umbra associates an individual layout setting for each scale.

derekbruening · 2020-06-19T19:21:42Z

It does, however, check all the scales (up 2x, down 2x, down 4x, down 8x) for any particular setting.

So the script already allows one to check a layout for a given scale. I can add support to the script to check all scales but I wonder what the benefit is because Umbra associates an individual layout setting for each scale.

That's not how I remember Umbra working: it tries to use the same setting for all scales, and only grudgingly makes an exception with a different displacement, having to do it just for one (or 2?) of the scales. Ideally there would be no exceptions, so I would want to see the results for all scales at once, preferring solutions with no exceptions.

johnfxgalea · 2020-06-20T04:40:42Z

It does, however, check all the scales (up 2x, down 2x, down 4x, down 8x) for any particular setting.

So the script already allows one to check a layout for a given scale. I can add support to the script to check all scales but I wonder what the benefit is because Umbra associates an individual layout setting for each scale.

That's not how I remember Umbra working: it tries to use the same setting for all scales, and only grudgingly makes an exception with a different displacement, having to do it just for one (or 2?) of the scales. Ideally there would be no exceptions, so I would want to see the results for all scales at once, preferring solutions with no exceptions.

Okay, no problem. I added the new option.

python3 umbra_layout.py --help
*** Umbra Shadow Memory Layout ***

usage: umbra_layout.py [-h] [--os {linux,windows8,windows81}] [--mask MASK]
                       [--disp DISP]
                       [--scale {all,down_8x,down_4x,down_2x,same,up_2x,up_4x,up_8x}]
                       [--verify] [--shadow_collision] [--max MAX]
                       [--unit UNIT] [--count COUNT]

Facilitates the set up of shadow memory layouts based on direct
mappings.Mappings are based on known Application Regions typically set up by
the OS. SHDW(app) = (app & MASK) + DISP

optional arguments:
  -h, --help            show this help message and exit
  --os {linux,windows8,windows81}
                        the operating system to consider.
  --mask MASK           the mask value applied to the app address.
  --disp DISP           the displacement value used for shadow translation.
  --scale {all,down_8x,down_4x,down_2x,same,up_2x,up_4x,up_8x}
                        scale of shadow memory with respect to app memory.
  --verify              verifies whether or not the passed value results ina
                        shadow memory layout without any collisions. If no
                        disp or mask values are passed, they will
                        besynthesized with appropriate values automatically.
                        Current implementation does not check formultiple
                        maps.
  --shadow_collision    Denotes whether to detect collisions with shadow's
                        shadow.
  --max MAX             specifies the max limit of a disp when in find mode.
  --unit UNIT           specifies the size of a unit.
  --count COUNT         specifies the number of maps.

I think the current implementation of Umbra tries the same setting for all scales by design, but on Linux, a different displacement value is used for each scale:

drmemory/umbra/umbra_64.c

Line 329 in 2d1e0a5

0x0000900000000000, /* UMBRA_MAP_SCALE_DOWN_8X */

Interestingly, the script manages to synthesize a displacement value that should be suitable for all scales, assuming only one shadow map is registered.

python3 umbra_layout.py --os linux --mask 0xFFFFFFFFFFF --verify --scale all --count 1
*** Umbra Shadow Memory Layout ***

OS: linux 

SUCCESS
Memory Layout:
	Mask: 0x00000FFFFFFFFFFF
	Disp: 0x0000080000000000
	Unit Size: 0x0000100000000000
	Scale UP: False
	Scale: 3


MAP 0
	app0:	 [0x0000000000000000, 0x0000010000000000] : exec,heap, data
	shd0:	 [0x0000010000000000, 0x0000012000000000]


	app1:	 [0x0000550000000000, 0x0000570000000000] : pie
	shd1:	 [0x000001A000000000, 0x000001E000000000]


	app2:	 [0x00007F0000000000, 0x0000800000000000] : lib, map, stack, vdso
	shd2:	 [0x000002E000000000, 0x0000030000000000]


Memory Layout:
	Mask: 0x00000FFFFFFFFFFF
	Disp: 0x0000080000000000
	Unit Size: 0x0000100000000000
	Scale UP: False
	Scale: 2


MAP 0
	app0:	 [0x0000000000000000, 0x0000010000000000] : exec,heap, data
	shd0:	 [0x0000020000000000, 0x0000024000000000]


	app1:	 [0x0000550000000000, 0x0000570000000000] : pie
	shd1:	 [0x0000034000000000, 0x000003C000000000]


	app2:	 [0x00007F0000000000, 0x0000800000000000] : lib, map, stack, vdso
	shd2:	 [0x000005C000000000, 0x0000060000000000]


Memory Layout:
	Mask: 0x00000FFFFFFFFFFF
	Disp: 0x0000080000000000
	Unit Size: 0x0000100000000000
	Scale UP: False
	Scale: 1


MAP 0
	app0:	 [0x0000000000000000, 0x0000010000000000] : exec,heap, data
	shd0:	 [0x0000040000000000, 0x0000048000000000]


	app1:	 [0x0000550000000000, 0x0000570000000000] : pie
	shd1:	 [0x0000068000000000, 0x0000078000000000]


	app2:	 [0x00007F0000000000, 0x0000800000000000] : lib, map, stack, vdso
	shd2:	 [0x00000B8000000000, 0x00000C0000000000]


Memory Layout:
	Mask: 0x00000FFFFFFFFFFF
	Disp: 0x0000080000000000
	Unit Size: 0x0000100000000000
	Scale UP: True
	Scale: 0


MAP 0
	app0:	 [0x0000000000000000, 0x0000010000000000] : exec,heap, data
	shd0:	 [0x0000080000000000, 0x0000090000000000]


	app1:	 [0x0000550000000000, 0x0000570000000000] : pie
	shd1:	 [0x00000D0000000000, 0x00000F0000000000]


	app2:	 [0x00007F0000000000, 0x0000800000000000] : lib, map, stack, vdso
	shd2:	 [0x0000170000000000, 0x0000180000000000]


Memory Layout:
	Mask: 0x00000FFFFFFFFFFF
	Disp: 0x0000080000000000
	Unit Size: 0x0000100000000000
	Scale UP: True
	Scale: 1


MAP 0
	app0:	 [0x0000000000000000, 0x0000010000000000] : exec,heap, data
	shd0:	 [0x0000100000000000, 0x0000120000000000]


	app1:	 [0x0000550000000000, 0x0000570000000000] : pie
	shd1:	 [0x00001A0000000000, 0x00001E0000000000]


	app2:	 [0x00007F0000000000, 0x0000800000000000] : lib, map, stack, vdso
	shd2:	 [0x00002E0000000000, 0x0000300000000000]


Memory Layout:
	Mask: 0x00000FFFFFFFFFFF
	Disp: 0x0000080000000000
	Unit Size: 0x0000100000000000
	Scale UP: True
	Scale: 2


MAP 0
	app0:	 [0x0000000000000000, 0x0000010000000000] : exec,heap, data
	shd0:	 [0x0000200000000000, 0x0000240000000000]


	app1:	 [0x0000550000000000, 0x0000570000000000] : pie
	shd1:	 [0x0000340000000000, 0x00003C0000000000]


	app2:	 [0x00007F0000000000, 0x0000800000000000] : lib, map, stack, vdso
	shd2:	 [0x00005C0000000000, 0x0000600000000000]


Memory Layout:
	Mask: 0x00000FFFFFFFFFFF
	Disp: 0x0000080000000000
	Unit Size: 0x0000100000000000
	Scale UP: True
	Scale: 3


MAP 0
	app0:	 [0x0000000000000000, 0x0000010000000000] : exec,heap, data
	shd0:	 [0x0000400000000000, 0x0000480000000000]


	app1:	 [0x0000550000000000, 0x0000570000000000] : pie
	shd1:	 [0x0000680000000000, 0x0000780000000000]


	app2:	 [0x00007F0000000000, 0x0000800000000000] : lib, map, stack, vdso
	shd2:	 [0x0000B80000000000, 0x0000C00000000000]

If I try to consider additional maps, separated by 2 units, a single setting for all scales seems to be unsat on Linux.

python3 umbra_layout.py --os linux --mask 0xFFFFFFFFFFF --verify --scale all --count 2
*** Umbra Shadow Memory Layout ***

OS: linux 

FAILED

derekbruening · 2020-11-30T04:56:58Z

@johnfxgalea -- is this mergeable? It may be very useful for #2328 where shadow layout problems are blocking us.

johnfxgalea · 2020-11-30T08:30:24Z

Yep, it is ready to be merged but still awaiting a review I think.

derekbruening · 2020-11-30T15:41:35Z

Yep, it is ready to be merged but still awaiting a review I think.

Oh, whoops. Though no longer sure #2328 is really a layout issue: may instead be an initialization/address walk issue at init time.

tools/umbra_layout.py

johnfxgalea · 2020-12-05T14:19:00Z

Done. PTAL. I added some further comments.

derekbruening

(Unfotunately the CI has been in bad shape for a while...I moved unix to Github Actions, and am trying to move Windows there and make it green too, but there are many problems to resolve.)

derekbruening · 2020-12-07T16:46:29Z

Xref #1712: we're hitting umbra shadow mapping failures up front on Linux on Github Actions.

derekbruening · 2021-01-03T17:56:29Z

I thought I got Windows green -- are those flakes? Add to the ignore list?

johnfxgalea · 2021-01-03T18:42:57Z

I thought I got Windows green -- are those flakes? Add to the ignore list?

Does not seem to be a flake, with the following stable error:

Exception calling "DownloadFile" with "2" argument(s): "The remote server returned an error: (404) Not Found."

johnfxgalea · 2021-01-05T15:53:39Z

I thought I got Windows green -- are those flakes? Add to the ignore list?

Does not seem to be a flake, with the following stable error:

Exception calling "DownloadFile" with "2" argument(s): "The remote server returned an error: (404) Not Found."

@derekbruening Any idea what the above error is about please? Happy to investigate further, but just wondering if you have any idea?

derekbruening · 2021-01-05T16:04:49Z

I thought I got Windows green -- are those flakes? Add to the ignore list?

Does not seem to be a flake, with the following stable error:
Exception calling "DownloadFile" with "2" argument(s): "The remote server returned an error: (404) Not Found."

@derekbruening Any idea what the above error is about please? Happy to investigate further, but just wondering if you have any idea?

If that's downloading doxygen is it related to DynamoRIO/dynamorio#4654?

johnfxgalea · 2021-01-05T19:08:32Z

I thought I got Windows green -- are those flakes? Add to the ignore list?

Does not seem to be a flake, with the following stable error:
Exception calling "DownloadFile" with "2" argument(s): "The remote server returned an error: (404) Not Found."

@derekbruening Any idea what the above error is about please? Happy to investigate further, but just wondering if you have any idea?

If that's downloading doxygen is it related to DynamoRIO/dynamorio#4654?

No. Dr Memory's CI is making use of a stale URL (http://doxygen.nl/files/doxygen-1.8.19.windows.x64.bin.zip) here:

drmemory/.github/workflows/ci-windows.yml

Line 64 in 04b22ef

    
                   (New-Object System.Net.WebClient).DownloadFile("http://doxygen.nl/files/doxygen-1.8.19.windows.x64.bin.zip", "c:\projects\install\doxygen.zip")

derekbruening · 2021-01-05T19:24:11Z

No. Dr Memory's CI is making use of a stale URL (http://doxygen.nl/files/doxygen-1.8.19.windows.x64.bin.zip) here:

drmemory/.github/workflows/ci-windows.yml

Line 64 in 04b22ef

(New-Object System.Net.WebClient).DownloadFile("http://doxygen.nl/files/doxygen-1.8.19.windows.x64.bin.zip", "c:\projects\install\doxygen.zip")

Ah yeah it needs the equiv of PR DynamoRIO/dynamorio#4643

johnfxgalea · 2021-01-06T09:51:12Z

CI failures concern #2250 and #2341

This PR does not concern these issues.

johnfxgalea added 3 commits June 19, 2020 10:37

Add script

2d7d15f

Arrange further code - mainly print statements

2fcbb9d

Remove trailing spaces

42792ef

derekbruening mentioned this pull request Jun 19, 2020

Umbra shadow layout exploration tool #2301

Closed

Add fixes and check all scales option

96f1815

johnfxgalea and others added 8 commits June 20, 2020 09:09

Add yapf command

27bf110

Arrange print messages

65a2d5c

Add more comments

00634fc

Fix typos

2222e43

Import sys

55eaf9d

Add more scales

c54b6cf

Remove shadow of shadow collisions

bc239a3

Don't mod sign bit

ffd3aae

Merge branch 'master' into i2283-umbra-layout-verify

dc66cee

derekbruening reviewed Nov 30, 2020

View reviewed changes

tools/umbra_layout.py Outdated Show resolved Hide resolved

tools/umbra_layout.py Show resolved Hide resolved

tools/umbra_layout.py Outdated Show resolved Hide resolved

derekbruening mentioned this pull request Dec 3, 2020

Move shadow translation endpoint tweak out of translation routine #2330

Open

Add review changes

2d21305

derekbruening approved these changes Dec 5, 2020

View reviewed changes

derekbruening and others added 2 commits December 5, 2020 14:45

Merge branch 'master' into i2283-umbra-layout-verify

ef8db94

Arrange code

8208d4a

:Merge branch 'master' into i2283-umbra-layout-verify

8b48abf

Split app3 region.

64ea4d6

Add issue number

d81394c

Merge branch 'master' into i2283-umbra-layout-verify

6f1b5a8

johnfxgalea merged commit b49b25d into master Jan 6, 2021

johnfxgalea deleted the i2283-umbra-layout-verify branch January 6, 2021 09:53

derekbruening mentioned this pull request Jan 16, 2021

umbra mapping fails when vdso is placed in 0x7fff'ff4-0x7fff'ff8 gap #2363

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

i#2283: Facilitate Umbra Layouts with Constraint Solving. #2300

i#2283: Facilitate Umbra Layouts with Constraint Solving. #2300

johnfxgalea commented Jun 19, 2020 •

edited

Loading

derekbruening commented Jun 19, 2020

johnfxgalea commented Jun 19, 2020

derekbruening commented Jun 19, 2020

johnfxgalea commented Jun 20, 2020 •

edited

Loading

derekbruening commented Nov 30, 2020

johnfxgalea commented Nov 30, 2020

derekbruening commented Nov 30, 2020

johnfxgalea commented Dec 5, 2020

derekbruening left a comment

derekbruening commented Dec 7, 2020

derekbruening commented Jan 3, 2021

johnfxgalea commented Jan 3, 2021

johnfxgalea commented Jan 5, 2021

derekbruening commented Jan 5, 2021

johnfxgalea commented Jan 5, 2021 •

edited

Loading

derekbruening commented Jan 5, 2021 •

edited

Loading

johnfxgalea commented Jan 6, 2021

i#2283: Facilitate Umbra Layouts with Constraint Solving. #2300

i#2283: Facilitate Umbra Layouts with Constraint Solving. #2300

Conversation

johnfxgalea commented Jun 19, 2020 • edited Loading

derekbruening commented Jun 19, 2020

johnfxgalea commented Jun 19, 2020

derekbruening commented Jun 19, 2020

johnfxgalea commented Jun 20, 2020 • edited Loading

derekbruening commented Nov 30, 2020

johnfxgalea commented Nov 30, 2020

derekbruening commented Nov 30, 2020

johnfxgalea commented Dec 5, 2020

derekbruening left a comment

Choose a reason for hiding this comment

derekbruening commented Dec 7, 2020

derekbruening commented Jan 3, 2021

johnfxgalea commented Jan 3, 2021

johnfxgalea commented Jan 5, 2021

derekbruening commented Jan 5, 2021

johnfxgalea commented Jan 5, 2021 • edited Loading

derekbruening commented Jan 5, 2021 • edited Loading

johnfxgalea commented Jan 6, 2021

johnfxgalea commented Jun 19, 2020 •

edited

Loading

johnfxgalea commented Jun 20, 2020 •

edited

Loading

johnfxgalea commented Jan 5, 2021 •

edited

Loading

derekbruening commented Jan 5, 2021 •

edited

Loading