Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Possibly incorrect allocation in function pp_alloc_clr #199

Closed
nkosmatov opened this issue Dec 26, 2024 · 2 comments
Closed

Possibly incorrect allocation in function pp_alloc_clr #199

nkosmatov opened this issue Dec 26, 2024 · 2 comments

Comments

@nkosmatov
Copy link
Contributor

While working on formal verification of cache coloring and page coloring mechanisms in Bao, we discovered two issues in function pp_alloc_clr

The following line (currently line 138 in commit c306b0f in file src/core/mmu/mem.c)
index ++;

should be removed. Otherwise , in some situations, a previously allocated page can be allocated again, or other unintended behavior can occur.

The following line (currently line 161 in commit c306b0f in file src/core/mmu/mem.c)
index = 0;
should be replaced by
index = pp_next_clr ( pool->base , 0 , colors ) ;
Otherwise , in some situations, a previously allocated page can be allocated again.

After the proposed modifications we were able to prove a (slightly simplified) corrected version of cache coloring and page coloring mechanisms in Bao.

@josecm
Copy link
Member

josecm commented Dec 26, 2024

Hello @nkosmatov!

After the proposed modifications we were able to prove a (slightly simplified) corrected version of cache coloring and page coloring mechanisms in Bao.

This is amazing!! Thank you for doing that work.

Your corrections seem to make sense. I'd propose you send a PR with the fixes you point out.

nkosmatov added a commit to nkosmatov/bao-hypervisor that referenced this issue Jan 2, 2025
josecm pushed a commit to nkosmatov/bao-hypervisor that referenced this issue Jan 6, 2025
See issue bao-project#199

Signed-off-by: Nikolai Kosmatov <[email protected]>
Signed-off-by: Jose Martins <[email protected]>
josecm pushed a commit to nkosmatov/bao-hypervisor that referenced this issue Jan 6, 2025
See issue bao-project#199

Signed-off-by: Nikolai Kosmatov <[email protected]>
Signed-off-by: Jose Martins <[email protected]>
josecm pushed a commit that referenced this issue Jan 6, 2025
See issue #199

Signed-off-by: Nikolai Kosmatov <[email protected]>
Signed-off-by: Jose Martins <[email protected]>
@josecm
Copy link
Member

josecm commented Jan 6, 2025

Fixed by #202

@josecm josecm closed this as completed Jan 6, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants