On Fri, Aug 12 2016, Michael S. Tsirkin wrote:

> On Tue, Jul 19, 2016 at 10:32:51AM -0500, Eric W. Biederman wrote:
>> I would really like to get a feel among kernel maintainers and
>> developers if this is something that is interesting, and what kind of
>> constraints they think something like this would need to be usable for
>> the kernel?
>> 
>> Eric
>
> Surprised that no one mentioned this yet - I think tagging
> integers/structs as coming from userspace could be useful,
> if we can teach e.g. smatch that access to a kernel
> pointer through this offset might fault.

We already have that.
Sparse recognizes
    __attribute__((noderef, address_space(1)))
 to mean "this is a pointer to a different address space which
 cannot be dereferened" and linux has

# define __user                __attribute__((noderef, address_space(1)))

so if you mark a pointer as "__user", then sparse will complain
if you dereference it.

We've had this for over a decade :-)

  https://lwn.net/Articles/87538/

NeilBrown