Powered by Linux
[PATCH 0/1] New smatch pattern for Confidential Cloud Computing — Semantic Matching Tool

[PATCH 0/1] New smatch pattern for Confidential Cloud Computing

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]


Hi Dan,

I would like to share and ask for the feedback on a new smatch kernel
pattern that we have written to facilitate the audit and
fuzzing of the new attack surface
between an untrusted host/VMM and a protected guest that exists
in various Confidential Cloud Computing solutions, such as
AMD SEV and Intel TDX. This pattern only attempts to capture various
locations where potentially untrusted inputs might be consumed by the
guest kernel and propagated within a single function. It does not
attempt to flag any real issues (for example out of bounds accesses),
but we use it to make sure all the code that is invoked into handling
an untrusted input is audited and reached by various fuzzers we have.
For flagging the real issues and proper taint propagation, I think we
would need to have smth similar that smatch already has for the user
data propagation (smatch_kernel_user_data.c, smatch_points_to_user_data.c).
I have made a quick proof of concept of trying
to modify the above user code to work for host input functions, but it does not
fully work easily out of the box (I can see some issues on arg propagation, etc.).
I think I am just still missing smth obvious on how it works with the database.
I will send the code I have in a separate patch to show my attempt. But since
the bulk of the code is clearly similar between the user and host data tracing,
I wonder what is the proper way to organize this into a common code?
I think it would be nice to have an abstraction layer that can perform
all the basic tainting and then separate modules to specify/drive what type of
data we want to taint (host inputs, user inputs, smth else potentially in the future?).

Once the full tainting and propagation are in order, then I think existing patterns
can be easily made to work with host input in the same way as with user input.
For example, I have tried it with specte v1 check_spectre.c pattern using
my trial smatch_kernel_host_data.c/point_to_host_data.c and was able to
find some potential spectre gadgets that are affected by host input.

I will be interested to work on this further with your guidance,
if you consider this suitable and useful for smatch to have.
We certainly think the host/guest attack surface is going to become
a very important attack surface going forward given the confidential
computing trend and its needs.

Best Regards,

Elena Reshetova (1):
  check_host_input: add a pattern

 check_host_input.c | 886 +++++++++++++++++++++++++++++++++++++++++++++
 check_list.h       |   2 +
 2 files changed, 888 insertions(+)
 create mode 100644 check_host_input.c


[Index of Archives]     [Linux USB Devel]     [Linux Audio Users]     [Yosemite News]     [Linux Kernel]     [Linux SCSI]     [Big List of Linux Books]

  Powered by Linux