Page MenuHomeFreeBSD

Added SAL annotatations to system calls
ClosedPublic

Authored by talg_cs.stanford.edu on Feb 9 2018, 7:36 PM.
Tags
None
Referenced Files
Unknown Object (File)
Thu, Nov 14, 7:27 AM
Unknown Object (File)
Mon, Nov 4, 12:46 PM
Unknown Object (File)
Wed, Oct 30, 11:21 PM
Unknown Object (File)
Sun, Oct 27, 9:06 PM
Unknown Object (File)
Sun, Oct 20, 7:58 AM
Unknown Object (File)
Fri, Oct 18, 2:29 PM
Unknown Object (File)
Fri, Oct 18, 1:03 AM
Unknown Object (File)
Oct 17 2024, 1:08 PM

Details

Summary

Add SAL annotatations to most system calls declarations (STD, NOSTD, COMPAT*) in
syscalls.master.

Modify makesyscalls.sh to strip out SAL annotations.

This is based on work I started in CheriBSD and use to validate fat
pointers at the syscall boundary. Tal Garfinkel reviewed the changes,
added annotations to COMPAT* syscalls and is using them in a record and
playback framework. One can envision other uses such as a WITNESS-like
validator for copyin/out as speculated on in the review.

As this time we are only annotating sys/kern/syscalls.master as that is
sufficient for userspace work. If kernel use cases materialize, we can
annotate other syscalls.master as needed.

Submitted by: Tal Garfinkel <talg@cs.stanford.edu>
Sponsored by: DARPA, AFRL (in part)

Test Plan

Running make sysent and looking at git status to ensure that the changes
have not impacted output of makesyscalls.sh.

Diff Detail

Lint
Lint Passed
Unit
No Test Coverage
Build Status
Buildable 15290
Build 15348: arc lint + arc unit

Event Timeline

There are a very large number of changes, so older changes are hidden. Show Older Changes
  • added missing annotations for send and recv.
cem added a subscriber: cem.

Seems fine in principle. I haven't audited the entire table for correctness. It would be good to document the available annotations and what they mean somewhere (a manual page?).

This revision is now accepted and ready to land.Mar 3 2018, 5:55 AM

Keep in mind the compat32 and Linux syscall tables could benefit from a very similar treatment.

I think some sort of reference to what SAL annotations are and where they are defined would be useful, probably in the commit message, but possibly also in the leading comment block of syscalls.master itself.

In D14285#306247, @jhb wrote:

I think some sort of reference to what SAL annotations are and where they are defined would be useful, probably in the commit message, but possibly also in the leading comment block of syscalls.master itself.

I'd argue for having the reference in the comment block.

  • added annotatations for gethostname, sethostname, revoke, pathconf.
This revision now requires review to proceed.Mar 5 2018, 10:03 PM
  • Added a note about SAL annotations to header comments re: emaste and jhb's comments.

I think it would be good to describe at least _In_, _Inout_, _Out_, and _opt_ annotation components not just that they are SAL 2.0 annotations since SAL doesn't google very well.

I think it would be good to describe at least _In_, _Inout_, _Out_, and _opt_ annotation components not just that they are SAL 2.0 annotations since SAL doesn't google very well.

I might as well describe them all. Given that we use such a small subset of SAL it will probably be much easier for future readers.

sys/kern/syscalls.master
534

drop this comment

945

drop |STD

1079

TMI?

  • Added documentation for annotations to header comment block.
  • -added annotations for remaining calls of type COMPAT and STD for consistency/completeness.
  • fixed incorrect annotation for cpuset_getdomain.
  • tiny wording change in documentation.
  • replaced tab with spaces for uniform formatting.
-rebased against latest HEAD.

If everyone is happy with the documentation and new annotations I think this is ready to land.

  • Added SAL annotations for COMPAT11 syscalls.

Some general comments:

  • NOSTD syscalls should definitely be annotated as they are current.
  • I think it would be best if the remaining COMPAT* ones were annotated as well.
  • When I look at the patched file in an editor, I see quite a few lines that extend beyond 80 columns. That should be fixed for lines that are newly too long. I know some of those are my fault...
sys/kern/syscalls.master
25

Don't make unrelated changes in this diff.

95

I'd leave this comment in.

169

I think we should infact go with _In_z_ here. I now believe it's the correct usage.

580–586

This comment was incorrectly restored.

593

this one too.

1079

We can remove this comment.

  • addresses brook's comments.
  • adds annotations for COMPAT* i.e. COMPAT10,7,...
  • adds annotations for NOSTD calls
  • reformats everything to not exceed 80 columns.
  • adds/removes some comments.
  • also fixes annotation for pwrite

This is getting close. In addition to (hopefully small) issues I've noted, another rebase is needed because getrandom has been added and needs annotation.

sys/kern/syscalls.master
110

Wrong indention and several other places. Continuing definitions should all be indented with <tab><tab><tab><tab><space><space><space><space>

205

Looks like a NOPARSE slipped through from CheriBSD

206

missing annotation on addr. That being said, there doesn't really seem to be a valid SAL annotation for the addr arguments of the mmap family. I'm not sure if we should use _In_ somewhat misleadingly or use something else like I did in CheriBSD.

What does your framework need to know about these addresses?

233

Not an issue with the change, but this isn't quite true to reality. Some programs allocate truncated fd_sets and the kernel needs to cope with this. Such programs shouldn't almost certainly use poll.

243–244

missing space before \

274

msg is a pointer and requires annotation. Other unannotated caddr_ts exist (at least recvfrom at 125)

346

extra space before comma

566

missing annotation.

661

no need to split this line.

  • formatting fixed a few missing annotations added.
  • -rebased against master to pull in getrandom and added annotation.

sorry about dribbling in the last set of fixes. that should address all the issues raised.

sys/kern/syscalls.master
206

We only care about _Out_* and _Inout_* parameters since we are only recording the results of system calls, not their inputs. So I'm neutral on the topic.

  • rebase
  • Whitespace fixes.
  • Fix getrandom annotation syntax.
  • Fix getrandom() whitespace.

This could probably use another review with fresh eyes for whitespace and missing annotations, but I think it's otherwise ready to land.

I'm sending out a final call for objections to freebsd-arch and plan to commit early next week.

This revision is now accepted and ready to land.Mar 30 2018, 8:35 PM
This revision was automatically updated to reflect the committed changes.