Misra R17.1 in Xen

Misra R17.1 in Xen

[Andrew Cooper]

Hello,

The x86_64-allcode run highlights one new violation of R17.1,
vmcoreinfo_append_str().  In writing this email, I've found another in
debugtrace_printk() meaning that we're missing some options in the
-allcode configuration.

In deviations.ecl we have:

-doc_begin="printf()-like functions are allowed to use the variadic features provided by stdarg.h."
-config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printk\\(.*\\)$)))"}
-config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printf\\(.*\\)$)))"}
-config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(panic)&&kind(function))))"}
-config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(elf_call_log_callback)&&kind(function))))"}
-config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(vprintk_common)&&kind(function))))"}
-config=MC3A2.R17.1,macros+={hide , "^va_(arg|start|copy|end)$"}
-doc_end


First, we have no printf() so that row should be removed.

But, more importantly this is safe if and only if the function
declaration uses __attribute__((__format__(printf, ...))) to cause the
compiler to perform format typechecking.

Is it possible to encode this attribute requirement in the Eclair
expression, so that e.g. accidentally dropping the attribute causes a
violation to be reported?  This would also be rather safer than assuming
that any prefix on printk() is safe.

Thanks,

~Andrew

Re: Misra R17.1 in Xen

[Nicola Vetrini]

On 2025-12-30 18:05, Andrew Cooper wrote:
> Hello,
> 
> The x86_64-allcode run highlights one new violation of R17.1,
> vmcoreinfo_append_str().  In writing this email, I've found another in
> debugtrace_printk() meaning that we're missing some options in the
> -allcode configuration.
> 
> In deviations.ecl we have:
> 
> -doc_begin="printf()-like functions are allowed to use the variadic 
> features provided by stdarg.h."
> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printk\\(.*\\)$)))"}
> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printf\\(.*\\)$)))"}
> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(panic)&&kind(function))))"}
> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(elf_call_log_callback)&&kind(function))))"}
> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(vprintk_common)&&kind(function))))"}
> -config=MC3A2.R17.1,macros+={hide , "^va_(arg|start|copy|end)$"}
> -doc_end
> 
> 
> First, we have no printf() so that row should be removed.
> 

I think it was for other variants of printf that are present in Xen 
(e.g. vsnprintf). Perhaps it could be restricted a bit to be more 
explicit.

> But, more importantly this is safe if and only if the function
> declaration uses __attribute__((__format__(printf, ...))) to cause the
> compiler to perform format typechecking.
> 
> Is it possible to encode this attribute requirement in the Eclair
> expression, so that e.g. accidentally dropping the attribute causes a
> violation to be reported?  This would also be rather safer than 
> assuming
> that any prefix on printk() is safe.
> 

Well, the UBs associated to that rule (to varargs in general) go beyond 
the formatting issues, but checking that the function decl has the 
attribute is a good suggestion to harden these deviations. I'll make 
some experiments and report back on this thread.

> Thanks,
> 
> ~Andrew

-- 
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253

Re: Misra R17.1 in Xen

[Nicola Vetrini]

On 2025-12-30 18:34, Nicola Vetrini wrote:
> On 2025-12-30 18:05, Andrew Cooper wrote:
>> Hello,
>> 
>> The x86_64-allcode run highlights one new violation of R17.1,
>> vmcoreinfo_append_str().  In writing this email, I've found another in
>> debugtrace_printk() meaning that we're missing some options in the
>> -allcode configuration.
>> 
>> In deviations.ecl we have:
>> 
>> -doc_begin="printf()-like functions are allowed to use the variadic 
>> features provided by stdarg.h."
>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printk\\(.*\\)$)))"}
>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printf\\(.*\\)$)))"}
>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(panic)&&kind(function))))"}
>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(elf_call_log_callback)&&kind(function))))"}
>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(vprintk_common)&&kind(function))))"}
>> -config=MC3A2.R17.1,macros+={hide , "^va_(arg|start|copy|end)$"}
>> -doc_end
>> 
>> 
>> First, we have no printf() so that row should be removed.
>> 
> 
> I think it was for other variants of printf that are present in Xen 
> (e.g. vsnprintf). Perhaps it could be restricted a bit to be more 
> explicit.
> 
>> But, more importantly this is safe if and only if the function
>> declaration uses __attribute__((__format__(printf, ...))) to cause the
>> compiler to perform format typechecking.
>> 
>> Is it possible to encode this attribute requirement in the Eclair
>> expression, so that e.g. accidentally dropping the attribute causes a
>> violation to be reported?  This would also be rather safer than 
>> assuming
>> that any prefix on printk() is safe.
>> 
> 
> Well, the UBs associated to that rule (to varargs in general) go beyond 
> the formatting issues, but checking that the function decl has the 
> attribute is a good suggestion to harden these deviations. I'll make 
> some experiments and report back on this thread.

Currently it is possible to match on the presence of the attribute 
"format", not on its arguments. Since "printf" is the only archetype 
used with "format" I don't think this is a big issue currently, but I'll 
let you be the judge on that.

> 
>> Thanks,
>> 
>> ~Andrew

-- 
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253

Re: Misra R17.1 in Xen

[Andrew Cooper]

On 30/12/2025 6:28 pm, Nicola Vetrini wrote:
> On 2025-12-30 18:34, Nicola Vetrini wrote:
>> On 2025-12-30 18:05, Andrew Cooper wrote:
>>> Hello,
>>>
>>> The x86_64-allcode run highlights one new violation of R17.1,
>>> vmcoreinfo_append_str().  In writing this email, I've found another in
>>> debugtrace_printk() meaning that we're missing some options in the
>>> -allcode configuration.
>>>
>>> In deviations.ecl we have:
>>>
>>> -doc_begin="printf()-like functions are allowed to use the variadic
>>> features provided by stdarg.h."
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printk\\(.*\\)$)))"}
>>>
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(^.*printf\\(.*\\)$)))"}
>>>
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(panic)&&kind(function))))"}
>>>
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(elf_call_log_callback)&&kind(function))))"}
>>>
>>> -config=MC3A2.R17.1,reports+={deliberate,"any_area(^.*va_list.*$&&context(ancestor_or_self(name(vprintk_common)&&kind(function))))"}
>>>
>>> -config=MC3A2.R17.1,macros+={hide , "^va_(arg|start|copy|end)$"}
>>> -doc_end
>>>
>>>
>>> First, we have no printf() so that row should be removed.
>>>
>>
>> I think it was for other variants of printf that are present in Xen
>> (e.g. vsnprintf). Perhaps it could be restricted a bit to be more
>> explicit.
>>
>>> But, more importantly this is safe if and only if the function
>>> declaration uses __attribute__((__format__(printf, ...))) to cause the
>>> compiler to perform format typechecking.
>>>
>>> Is it possible to encode this attribute requirement in the Eclair
>>> expression, so that e.g. accidentally dropping the attribute causes a
>>> violation to be reported?  This would also be rather safer than
>>> assuming
>>> that any prefix on printk() is safe.
>>>
>>
>> Well, the UBs associated to that rule (to varargs in general) go
>> beyond the formatting issues, but checking that the function decl has
>> the attribute is a good suggestion to harden these deviations. I'll
>> make some experiments and report back on this thread.
>
> Currently it is possible to match on the presence of the attribute
> "format", not on its arguments. Since "printf" is the only archetype
> used with "format" I don't think this is a big issue currently, but
> I'll let you be the judge on that.

There's scanf as the other option to format, but I suppose for the
specifics of a deviation for va_list, not being able to
match/distinguish format from scanf is fine.

~Andrew