Should Code Contracts be used for security?

Question

Are there any reasons why you wouldn't use Code Contracts to enforce business rules?

Imagine you have a User class that represents a single user of a system and defines actions that can be performed against other users. You could write a ChangePassword method like this...

public void ChangePassword(User requestingUser, string newPassword)
{
    Contract.Requires<ArgumentNullException>(requestingUser);
    Contract.Requires<ArgumentNullException>(newPassword);

    // Users can always change their own password, but they must be an
    // administrator to change someone else's.
    if (requestingUser.UserId != this.UserId &&
        !requestingUser.IsInRole("Administrator"))
        throw new SecurityException("You don't have permission to do that.");

    // Change the password.
    ...
}

Or you could implement the security check as a precondition with Contract.Requires...

public void ChangePassword(User requestingUser, string newPassword)
{
    Contract.Requires<ArgumentNullException>(requestingUser != null);
    Contract.Requires<ArgumentNullException>(newPassword != null);

    // Users can always change their own password, but they must be an
    // administrator to change someone else's.
    Contract.Requires<SecurityException>(
        requestingUser.UserId == this.UserId ||
        !requestingUser.IsInRole("Administrator"),
        "You don't have permission to do that.");

    // Change the password.
    ...
}

What are the advantages and disadvantages of these two methods?

Answer 1

I think the answer is no. Code Contracts are designed for scenarios where their failure indicates a serious bug in the code. They should not be something that can be recovered from such as incorrect user input.

Requires<T> is meant to be used only on public methods of a library that will be consumed by others who are not using Code Contracts, or if you have legacy code that needs to remain compatible in terms of what exceptions it can throw.

For new code, you should only be using Requires, not Requires<T>. Plain Requires throws an uncatchable exception by default, to force you to deal with the problem.

Furthermore, if someone disables Code Contracts runtime checking, all your security will disappear!