Page MenuHomeFreeBSD

Added SAL annotatations to system calls
ClosedPublic

Authored by talg_cs.stanford.edu on Feb 9 2018, 7:36 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

Repository
rS FreeBSD src repository
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.

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 accepted this revision.Mar 3 2018, 5:55 AM
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
cem added a comment.Mar 3 2018, 5:56 AM

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

emaste added a subscriber: emaste.Mar 4 2018, 2:01 AM
jhb added a subscriber: jhb.Mar 5 2018, 6:24 PM

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.

emaste added a comment.Mar 5 2018, 6:47 PM
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 ↗(On Diff #39104)

drop this comment

946 ↗(On Diff #39104)

drop |STD

1080 ↗(On Diff #39104)

TMI?

  • Added documentation for annotations to header comment block.
talg_cs.stanford.edu edited the summary of this revision. (Show Details)Mar 7 2018, 7:44 PM
  • -added annotations for remaining calls of type COMPAT and STD for consistency/completeness.
  • fixed incorrect annotation for cpuset_getdomain.
talg_cs.stanford.edu edited the summary of this revision. (Show Details)Mar 7 2018, 10:23 PM
  • tiny wording change in documentation.
  • replaced tab with spaces for uniform formatting.
talg_cs.stanford.edu updated this revision to Diff 40062.EditedMar 8 2018, 1:08 AM
-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.
talg_cs.stanford.edu edited the summary of this revision. (Show Details)Mar 9 2018, 12:10 AM

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
1080 ↗(On Diff #39104)

We can remove this comment.

25 ↗(On Diff #40092)

Don't make unrelated changes in this diff.

95 ↗(On Diff #40092)

I'd leave this comment in.

193 ↗(On Diff #40092)

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

609 ↗(On Diff #40092)

This comment was incorrectly restored.

623 ↗(On Diff #40092)

this one too.

talg_cs.stanford.edu edited the summary of this revision. (Show Details)Mar 16 2018, 7:28 PM
talg_cs.stanford.edu updated this revision to Diff 40356.EditedMar 16 2018, 8:08 PM
  • 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
141 ↗(On Diff #40356)

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

242 ↗(On Diff #40356)

Looks like a NOPARSE slipped through from CheriBSD

243 ↗(On Diff #40356)

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?

276 ↗(On Diff #40356)

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.

286 ↗(On Diff #40356)

missing space before \

322 ↗(On Diff #40356)

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

402 ↗(On Diff #40356)

extra space before comma

641 ↗(On Diff #40356)

missing annotation.

742 ↗(On Diff #40356)

no need to split this line.

  • formatting fixed a few missing annotations added.
  • removed line break.
  • -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
243 ↗(On Diff #40356)

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.

brooks updated this revision to Diff 40649.Mar 23 2018, 9:03 PM
  • rebase
  • Whitespace fixes.
brooks updated this revision to Diff 40650.Mar 23 2018, 9:04 PM
  • Fix getrandom annotation syntax.
brooks updated this revision to Diff 40651.Mar 23 2018, 9:06 PM
  • 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.

brooks accepted this revision.Mar 30 2018, 8:35 PM

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
brooks edited the summary of this revision. (Show Details)Apr 5 2018, 8:28 PM
This revision was automatically updated to reflect the committed changes.